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 c35cdb377d700c8df6de42375fa80a34617359ab..4f57d80ede454fae9f0e2403d37f17de00df6240 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+let use_stylesheets = ref false;;(* false performs the transformations in OCaml*)
+
 (* List utility functions *)
 exception Skip;;
 
@@ -145,7 +147,10 @@ class proof_viewer obj =
 
   inherit GMathViewAux.single_selection_math_view 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
@@ -185,6 +190,77 @@ class proof_viewer obj =
          end
     | None -> assert false (* "ERROR: No selection!!!" *)
 
+  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
+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,
@@ -197,10 +273,11 @@ class proof_viewer obj =
       ~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)
+    (acic, ids_to_inner_types, ids_to_inner_sorts)
  end
 ;;
 
@@ -226,3 +303,7 @@ let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
   end;
   mathview
 ;;
+
+let _ =
+ Cexpr2pres_hashtbl.init Cexpr2pres.cexpr2pres Cexpr2pres.cexpr2pres_charcount
+;;