Previous commit was erroneous and dit not compile.

Fixed.

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index d5950a1c9043cdd3985d3963e2b980f58e7c515c..06ba96a221da88f91ce8f623e1b4e634bcce00da 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -190,19 +190,17 @@ 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)
+  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
-prerr_endline "0000000000000000 USO GLI STYLESHEETS" ;
-     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" ;
@@ -216,76 +214,6 @@ prerr_endline "0000000000000000 CARICO L'mml PRODOTTO" ;
       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
-    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 "(******** INIZIO CONTENT ==> PRES **********)";
-     (*
-     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) ;