snapshot (notably: implemented "check")

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 28dee494728511a693ce7e6a9cb06cabb0ce276c..bf57dc8d91b1d7470117001c1893336550bf4844 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -52,11 +52,14 @@ let save_dom =
 
 (** {2 Initialization} *)
 
+let _ =
+  GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
+  GtkMain.Main.init ()
 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 gui = MatitaGui.instance ()
 let disambiguator =
   new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
     ~chooseUris:(interactive_user_uri_choice ~gui)
@@ -66,14 +69,17 @@ 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 sequents_viewer =
+  MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
+    ~sequent_viewer ()
 
 let new_proof (proof: MatitaTypes.proof) =
   let xmldump_observer _ _ =  print_endline proof#toString in
-  let proof_observer _ (status, metadata) =
+  let proof_observer _ (status, (proof_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)
+      proof_metadata
     in
     let ((uri_opt, _, _, _), _) = status in
     let uri = MatitaTypes.unopt_uri uri_opt in
@@ -83,72 +89,16 @@ let new_proof (proof: MatitaTypes.proof) =
         ~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;
+    proof_viewer#load_proof mathml proof_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"
+  let sequents_observer _ ((proof, goal_opt), (_, sequents_metadata)) =
+    sequents_viewer#reset;
+    (match goal_opt with
+    | None -> ()
+    | Some goal ->
+        sequents_viewer#load_sequents sequents_metadata;
+        sequents_viewer#goto_sequent goal)
   in
   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
       sequents_observer);
@@ -167,7 +117,10 @@ let quit () = (* quit program, asking for confirmation if needed *)
     GMain.Main.quit ()
 
 let abort_proof () =
-  MatitaTypes.not_implemented "Matita.abort_proof"
+  if has_proof () then begin
+    set_proof None;
+    sequents_viewer#reset
+  end
 
 let proof_handler =
   { MatitaTypes.get_proof = get_proof;