Now applying ocaml transformations to sequents as well.

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index e105d5f0ea32ef9a3df3b50b66a1e6bd80872628..409c7cd70f4a82ad2aa587cf89acfeb815883d89 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -23,15 +23,14 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 29/01/2003                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(***************************************************************************)
+(*                                                                         *)
+(*                             PROJECT HELM                                *)
+(*                                                                         *)
+(*                  29/01/2003 Claudio Sacerdoti Coen                      *)
+(*                                                                         *)
+(*                                                                         *)
+(***************************************************************************)
 
 let use_stylesheets = ref false;;(* false performs the transformations in OCaml*)
 
@@ -109,8 +108,12 @@ class sequent_viewer obj =
      ) selections
   
   method load_sequent metasenv sequent =
+(**** SIAM QUI ****)
    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
-    ApplyStylesheets.mml_of_cic_sequent metasenv sequent
+     if !use_stylesheets then
+       ApplyStylesheets.mml_of_cic_sequent metasenv sequent
+     else 
+       ApplyTransformation.mml_of_cic_sequent metasenv sequent
    in
     self#load_doc ~dom:sequent_mml ;
 (*
@@ -204,81 +207,44 @@ class proof_viewer obj =
     | 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
-     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 **********)";
-             (match current_mml with
-                 None ->
-                  let time1 = Sys.time () in
-                  self#load_doc ~dom:mml ;
-                  let time2 = Sys.time () in
-                  prerr_endline ("Loading and displaying the proof took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
-                  current_mml <- Some mml
-               | Some current_mml' ->
-                  self#freeze ;
-                  let time1 = Sys.time () in
-                  XmlDiff.update_dom ~from:current_mml' mml ;
-                  let time2 = Sys.time () in
-                  prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
-                  self#thaw ;
-                  let time3 = Sys.time () in
-                  prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds")
-                  ) ;
-(*
-              self#load_doc ~dom:mml ;
-              current_mml <- Some 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);
+    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 =
+      if !use_stylesheets then
+        ApplyStylesheets.mml_of_cic_object
+          ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+      else 
+        ApplyTransformation.mml_of_cic_object
+          ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in
+    current_infos <-
+      Some
+       (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
+    (* self#load_doc ~dom:mml ;
+       current_mml <- Some mml ; *)
+    (match current_mml with
+      None ->
+        let time1 = Sys.time () in
+        self#load_doc ~dom:mml ;
+        let time2 = Sys.time () in
+        prerr_endline ("Loading and displaying the proof took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
+        current_mml <- Some mml
+    | Some current_mml' ->
+        self#freeze ;
+        let time1 = Sys.time () in
+        XmlDiff.update_dom ~from:current_mml' mml ;
+        let time2 = Sys.time () in
+        prerr_endline ("XMLDIFF took " ^ string_of_float (time2 -. time1) ^ "seconds") ;
+        self#thaw ;
+        let time3 = Sys.time () in
+        prerr_endline ("The refresh of the widget took " ^ string_of_float (time3 -. time2) ^ "seconds"));
     (acic, ids_to_inner_types, ids_to_inner_sorts)
- end
+  end
 ;;
 
+
 let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
   GtkBase.Container.make_params ~cont:(
   OgtkMathViewProps.pack_return