ocaml 3.09 transition

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

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 913cc95292023719004c229025e7692551b00283..0f2019ad507b3a3c2d6c9a850ca537001ce3eefd 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -38,18 +38,25 @@ let debug_print s = if debug then prerr_endline s
 type mml_of_cic_sequent =
  Cic.metasenv ->
  int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document * 
+ (Cic.annconjecture *
   ((Cic.id, Cic.term) Hashtbl.t *
    (Cic.id, Cic.id option) Hashtbl.t *
-   (string, Cic.hypothesis) Hashtbl.t)
+   (string, Cic.hypothesis) Hashtbl.t *
+   (Cic.id, string) Hashtbl.t))
+   
 
 type mml_of_cic_object =
-  explode_all:bool ->
-  UriManager.uri ->
-  Cic.annobj ->
-  (string, string) Hashtbl.t ->
-  (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-
+  Cic.obj ->
+  Gdome.document * 
+  (Cic.annobj * 
+   ((Cic.id, Cic.term) Hashtbl.t * 
+    (Cic.id, Cic.id option) Hashtbl.t *
+    (Cic.id, Cic.conjecture) Hashtbl.t * 
+    (Cic.id, Cic.hypothesis) Hashtbl.t *
+    (Cic.id, string) Hashtbl.t *   
+    (Cic.id, Cic2acic.anntypes) Hashtbl.t))
+  
 (* List utility functions *)
 exception Skip;;
 
@@ -86,7 +93,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
      (function node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -108,7 +115,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
      (function node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -124,13 +131,11 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
   
   method load_sequent metasenv sequent =
 (**** SIAM QUI ****)
-   let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+   let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) =
      mml_of_cic_sequent metasenv sequent
    in
     self#load_root ~root:sequent_mml#get_documentElement ;
-(*
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
-*)
+ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
@@ -190,7 +195,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
       Some node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -209,7 +214,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
       Some node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -223,21 +228,19 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) 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
-    let mml =
-      mml_of_cic_object
-        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+  method load_proof currentproof =
+    let mml,
+         (acic,
+           (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+            ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
+      mml_of_cic_object currentproof
     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 ; *)
+    ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
     (match current_mml with
       None ->
         let time1 = Sys.time () in