- 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"