snapshot, notably:

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f264ec413cad9c51932a3c804d3c88fe3ca60c9c..03803c2b94073eb3e5a72517fcda403e6b36516e 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -85,8 +85,17 @@ class clickable_math_view obj =
       | None   -> self#set_selection None
   end
 
+let clickable_math_view =
+  GtkBase.Widget.size_params
+    ~cont:(OgtkMathViewProps.pack_return (fun p ->
+      OgtkMathViewProps.set_params
+        (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p))
+        ~font_size:None ~log_verbosity:None))
+    []
+let clickable_math_view () = clickable_math_view ()
+
 class proof_viewer obj =
-  object(self)
+  object (self)
 
     inherit clickable_math_view obj
 
@@ -94,16 +103,14 @@ class proof_viewer obj =
     val mutable current_mathml = None
 
     method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
-      let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
-          ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
-        Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+      let uri = unopt_uri uri_opt in
+      let obj = cicCurrentProof proof in
+      let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+           ids_to_hypotheses)) =
+        ApplyTransformation.mml_of_cic_object uri obj
       in
       current_infos <- Some (ids_to_terms, ids_to_father_ids,
         ids_to_conjectures, ids_to_hypotheses);
-      let mathml =
-        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 ./proof";
       ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
       match current_mathml with
@@ -269,6 +276,18 @@ let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
         ~font_size ~log_verbosity))
     []
 
+class cicBrowser =
+  object (self)
+    val widget =
+      let gui = MatitaGui.instance () in
+      sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add ()
+
+    initializer
+      widget#set_href_callback (Some (fun uri -> self#load_uri uri))
+
+    method load_uri uri = ()
+  end
+
 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
@@ -284,11 +303,6 @@ let proof_viewer_instance =
   ) in
   fun () -> Lazy.force instance
 
-let sequents_viewer ~(notebook:GPack.notebook)
-  ~(sequent_viewer:sequent_viewer) ~set_goal ()
-=
-  new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
-
 class mathViewer =
   let href_callback: (UriManager.uri -> unit) option ref = ref None in
   object
@@ -314,5 +328,12 @@ class mathViewer =
     method unload () = (proof_viewer_instance ())#unload
   end
 
+let sequents_viewer ~(notebook:GPack.notebook)
+  ~(sequent_viewer:sequent_viewer) ~set_goal ()
+=
+  new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
+
 let mathViewer () = new mathViewer
 
+let cicBrowser () = new cicBrowser
+