snapshot, notably:

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index bb62f51c98d334818e64eb013b6300e0ca783e3e..d485ac02588c66e31510ed7a6d6fed2935122bb6 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -91,8 +91,8 @@ class proof_viewer obj =
       ApplyTransformation.mml_of_cic_object ~explode_all:true
         (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
     in
-    debug_print "load_proof: dumping MathML to /tmp/proof";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/proof" ~doc:mathml ());
+    debug_print "load_proof: dumping MathML to ./proof";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
     match current_mathml with
     |  None ->
         self#load_root ~root:mathml#get_documentElement ;
@@ -165,14 +165,14 @@ class sequent_viewer obj =
       ApplyTransformation.mml_of_cic_sequent metasenv sequent
     in
     current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
-    debug_print "load_sequent: dumping MathML to /tmp/prova";
-    ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mathml ());
+    debug_print "load_sequent: dumping MathML to ./prova";
+    ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
  end
 
 
 class sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
+  ~(sequent_viewer:sequent_viewer) ~set_goal ()
 =
   let tab_label metano =
     (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
@@ -237,7 +237,6 @@ class sequents_viewer ~(notebook:GPack.notebook)
       sequent_viewer#load_sequent _metasenv goal;
       try
         List.assoc goal goal2win ();
-        debug_print "set_selection none";
         sequent_viewer#set_selection None
       with Not_found -> assert false
 
@@ -278,7 +277,27 @@ let proof_viewer_instance =
   fun () -> Lazy.force instance
 
 let sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
+  ~(sequent_viewer:sequent_viewer) ~set_goal ()
 =
   new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
 
+let check_widget =
+  lazy
+    (let gui = MatitaGui.instance () in
+    sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add ())
+
+class mathViewer =
+  object
+    method checkTerm sequent metasenv =
+      let (metano, context, expr) = sequent in
+      let widget = Lazy.force check_widget in
+      let gui = MatitaGui.instance () in
+      gui#check#checkWin#show ();
+      gui#main#showCheckMenuItem#set_active true;
+      widget#load_sequent (sequent :: metasenv) metano
+
+    method unload () = (proof_viewer_instance ())#unload
+  end
+
+let mathViewer () = new mathViewer
+