Previous commit was erroneous and dit not compile.

[helm.git] / helm / gTopLevel / termViewer.ml

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 192bbb413b6d203eddfc48c1faa06d3c22670af8..06ba96a221da88f91ce8f623e1b4e634bcce00da 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -150,6 +150,7 @@ class proof_viewer obj =
   initializer self#set_font_size 10
 
   val mutable current_infos = None
+  val mutable current_mml = None
 
   method make_sequent_of_selected_term =
    match self#get_selection with
@@ -196,61 +197,26 @@ class proof_viewer obj =
    =
     Cic2acic.acic_object_of_cic_object currentproof
    in
-    if !use_stylesheets then
-     let mml =
-      ApplyStylesheets.mml_of_cic_object
-       ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
-     in
+    let mml =
+     ApplyStylesheets.mml_of_cic_object
+      ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+    in
+      (match current_mml with
+          None ->
+prerr_endline "0000000000000000 CARICO L'mml PRODOTTO" ;
+           self#load_doc ~dom:mml ;
+           current_mml <- Some mml
+        | Some current_mml ->
+           self#freeze ;
+           XmlDiff.update_dom ~from:current_mml mml ;
+           self#thaw) ;
+(*
       self#load_doc ~dom:mml ;
-      current_infos <-
-       Some
-        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
-    else
-     (match acic with
-         Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
-           let time1 = Sys.time () in
-           let content = 
-            Cic2content.acic2content 
-             (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts
-             ~ids_to_inner_types bo in
-           let content2pres =
-             (Content2pres.proof2pres 
-               (function p -> 
-                 (Cexpr2pres.cexpr2pres_charcount 
-                    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))) in
-           let pres = content2pres content in
-           let time2 = Sys.time () in
-           (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
-           let xmlpres =
-            Xml.xml_nempty "math"
-             ["xmlns","http://www.w3.org/1998/Math/MathML" ;
-              "xmlns:helm","http://www.cs.unibo.it/helm" ;
-              "xmlns:xlink","http://www.w3.org/1999/xlink"
-             ] (Mpresentation.print_mpres pres) in
-           let time25 = Sys.time () in
-            (*
-            prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
-            Xml.pp xmlpres (Some "tmp");
-            let time3 = Sys.time () in
-             prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25)));
-            *)
-           (try 
-             (* prerr_endline "(******** INIZIO DOM **********)"; *)
-             let mml = Xml2Gdomexmath.document_of_xml Misc.domImpl xmlpres in
-             let time3 = Sys.time () in
-             (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *)
-             (* prerr_endline "(******** FINE DOM **********)"; *)
-             self#load_doc ~dom:mml;
-             prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2)))
-            (*
-             self#load_uri "tmp";
-             let time4 = Sys.time () in
-             prerr_endline
-              ("Fine loading:" ^ (string_of_float (time4 -. time3)))
-            *)
-           with (GdomeInit.DOMException (_,s)) as e ->
-              prerr_endline s; raise e)
-       | _ -> assert false);
+      current_mml <- Some mml ;
+*)
+     current_infos <-
+      Some
+       (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
     (acic, ids_to_inner_types, ids_to_inner_sorts)
  end
 ;;