XmlDiff-ing of DOM trees implemented.

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

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index a54db659d60c8bab686eb021ae20ecc9807a611d..4f57d80ede454fae9f0e2403d37f17de00df6240 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
@@ -189,57 +190,93 @@ class proof_viewer obj =
          end
     | None -> assert false (* "ERROR: No selection!!!" *)
 
-  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
-    if !use_stylesheets then
+  method load_omdoc_proof uri ~ids_to_inner_sorts cobj =
+   if !use_stylesheets then
+    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 (Content2cic.cobj2obj cobj)
+    in
      let mml =
       ApplyStylesheets.mml_of_cic_object
        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
      in
       self#load_doc ~dom:mml ;
+      current_mml <- Some 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.annobj2content 
-                ~ids_to_inner_sorts ~ids_to_inner_types acic in
-           let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
-           let time2 = Sys.time () in
-           (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
-           let xmlpres = 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 = Xml2Gdome.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);
+   else
+prerr_endline "(******** INIZIO CONTENT ==> PRES **********)";
+    let pres = Content2pres.content2pres ~ids_to_inner_sorts cobj in
+    let time2 = Sys.time () in
+    (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
+    let xmlpres = 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 = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in
+      let time3 = Sys.time () in
+      (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *)
+      prerr_endline "(******** FINE DOM **********)";
+      (match current_mml with
+          None ->
+           self#load_doc ~dom:mml ;
+           current_mml <- Some mml
+        | Some current_mml ->
+           self#freeze ;
+prerr_endline "XML_DIFF: prima passata";
+(*
+ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_1.xml" ()) ;
+ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_1.xml" ()) ;
+*)
+           XmlDiff.update_dom ~from:current_mml mml ;
+(*
+prerr_endline "XML_DIFF: seconda passata";
+ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_2.xml" ()) ;
+ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_2.xml" ()) ;
+           XmlDiff.update_dom ~from:current_mml mml ;
+ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_3.xml" ()) ;
+ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_3.xml" ()) ;
+*)
+prerr_endline "XML_DIFF: fine passate";
+           self#thaw) ;
+(*
+      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)
+
+  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 =
+     ApplyStylesheets.mml_of_cic_object
+      ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+    in
+     self#load_doc ~dom:mml ;
+     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
 ;;