- let sequents_observer =
- let pages = ref 0 in
- let callback_id = ref None in
- let mathmls = ref [] in
- fun _ ((proof, goal_opt) as status, metadata) ->
- debug_print "sequents_observer";
- let notebook = gui#main#sequentsNotebook in
- for i = 1 to !pages do
- notebook#remove_page 0
- done;
- mathmls := [];
- (match !callback_id with
- | Some id -> GtkSignal.disconnect notebook#as_widget id
- | None -> ());
- if goal_opt <> None then begin
- let sequents = snd metadata in
- let sequents_no = List.length sequents in
- debug_print (sprintf "sequents no: %d" sequents_no);
- pages := sequents_no;
- let widget = sequent_viewer#coerce in
- List.iter
- (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
- let tab_label =
- (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
- in
- notebook#append_page ~tab_label widget;
- let mathml = lazy
- (let content_sequent = Cic2content.map_sequent asequent in
- let pres_sequent =
- Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
- in
- let xmlpres = Box.document_of_box pres_sequent in
- Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
- in
- mathmls := (metano, mathml) :: !mathmls)
- sequents;
- mathmls := List.rev !mathmls;
- let render_page page =
- let (metano, mathml) = List.nth !mathmls page in
- sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
- in
- callback_id :=
- (* TODO Zack the "#after" may probably be removed after Luca's fix for
- * widget not loading documents before being realized *)
- Some (notebook#connect#after#switch_page ~callback:(fun page ->
- debug_print "switch_page callback";
- render_page page));
- (match goal_opt with
- | Some goal -> (* current goal available, go to corresponding page *)
- let page = ref 0 in
- (try
- List.iter
- (fun (metano, _) ->
- if (metano = goal) then raise Exit;
- incr page)
- sequents;
- with Exit ->
- debug_print (sprintf "going to page %d" !page);
- notebook#goto_page !page;
- render_page !page)
- | None -> ());
- end;
- debug_print "/sequents_observer"
+ if success then
+ gui#lockScript (locked_iter#offset + interpreter#endOffset)
+
+let script_jump _ =
+ let buf = gui#script#scriptTextView#buffer in
+ let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
+ let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
+ let len = String.length raw_text in
+ let rec parse offset =
+ if offset < len then begin
+ let (success, hide) =
+ interpreter#evalPhrase (String.sub raw_text offset (len - offset))
+ in
+ if success then begin
+ let new_offset = interpreter#endOffset + offset in
+ gui#lockScript (new_offset + locked_iter#offset);
+ parse new_offset
+ end else
+ raise Exit
+ end