snapshot

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index c323dbbf05fc34604d45a205122192841d364b87..58a6f7a96b426d88470044b34e1ff9c304d0e27e 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -35,7 +35,7 @@
 open MatitaTypes
 
 (* List utility functions *)
-exception Skip;;
+exception Skip
 
 let list_map_fail f =
  let rec aux =
@@ -49,10 +49,11 @@ let list_map_fail f =
        (aux tl)
  in
   aux
-;;
+
 (* End of the list utility functions *)
 
-class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
+(*
+class sequent_viewer obj =
  object(self)
 
   inherit GMathViewAux.multi_selection_math_view obj
@@ -107,57 +108,55 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
-;;
+*)
 
-class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
+class proof_viewer obj =
  object(self)
 
   inherit GMathViewAux.single_selection_math_view obj
 
+(*   initializer self#set_log_verbosity 3 *)
+
   val mutable current_infos = None
   val mutable current_mml = None
 
-  method load_proof uri currentproof =
-    let
-      (acic,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 currentproof
-    in
-    let mml =
-      mml_of_cic_object
-        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+  method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
+    let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+        ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
+      metadata
     in
     current_infos <-
       Some
        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
-    (match current_mml with
-      None ->
+    match current_mml with
+    |  None ->
+        MatitaTypes.debug_print "no previous MathML";
         self#load_root ~root:mml#get_documentElement ;
         current_mml <- Some mml
     | Some current_mml' ->
+        MatitaTypes.debug_print "Previous MathML available: xmldiffing ...";
         self#freeze ;
         XmlDiff.update_dom ~from:current_mml' mml ;
-        self#thaw);
-    (acic, ids_to_inner_types, ids_to_inner_sorts)
+        self#thaw
   end
 
  (** constructors *)
 
-let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent) =
+(*
+let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
       OgtkMathViewProps.set_params
-        (new sequent_viewer ~mml_of_cic_sequent
-          (GtkMathViewProps.MathView_GMetaDOM.create p))
-        ?font_size:None ?log_verbosity:None))
-    ?width:None ?height:None []
+        (new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
+        ~font_size ~log_verbosity))
+    []
+*)
 
-let proof_viewer ~(mml_of_cic_object: mml_of_cic_object) =
+let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Widget.size_params
     ~cont:(OgtkMathViewProps.pack_return (fun p ->
       OgtkMathViewProps.set_params
-        (new proof_viewer ~mml_of_cic_object
-          (GtkMathViewProps.MathView_GMetaDOM.create p))
-        ?font_size:None ?log_verbosity:None))
-    ?width:None ?height:None []
+        (new proof_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
+        ~font_size ~log_verbosity))
+    []