-let _ = Helm_registry.load_from "matita.conf.xml"
-let _ = GMain.Main.init ()
-let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
-let parserr = new MatitaDisambiguator.parserr ()
-let mqiconn = MQIConn.init ()
-let disambiguator =
- new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
- ~chooseUris:(interactive_user_uri_choice ~gui)
- ~chooseInterp:(interactive_interp_choice ~gui)
- ()
-let proof_viewer =
- let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
- MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
-let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
-
-let new_proof (proof: MatitaTypes.proof) =
- let xmldump_observer _ _ = print_endline proof#toString in
- let proof_observer _ (status, metadata) =
- debug_print "proof_observer";
- let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- (fst metadata)
- in
- let ((uri_opt, _, _, _), _) = status in
- let uri = MatitaTypes.unopt_uri uri_opt in
- debug_print "apply transformation";
- let mathml =
- ApplyTransformation.mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
- in
- if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml";
- proof_viewer#load_proof mathml metadata;
- debug_print "/proof_observer"
- in
- 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"
- in
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- sequents_observer);
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- proof_observer);
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- xmldump_observer);
- proof#notify;
- set_proof (Some proof)