X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=23d7543d3da08d19995e393b4f69596febc01426;hb=3c9c376401844c389d682ba835845443105e4b1a;hp=4eac2617a6b4f9cff7949bf4b558715b651b6dc2;hpb=548d5244b8893cb51851383c30523271b7bd88a3;p=helm.git

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 4eac2617a..23d7543d3 100644
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -38,18 +38,26 @@ 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 +94,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 +116,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,12 +132,10 @@ 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
-prerr_endline "PRIMA DI SALVARE IL FILE" ;
     self#load_root ~root:sequent_mml#get_documentElement ;
-prerr_endline "SALVO IL FILE IN TEMP" ;
 ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
@@ -190,7 +196,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 +215,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!!!" *)
@@ -224,21 +230,18 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) 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
-    let mml =
-      mml_of_cic_object
-        ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+    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 uri 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 ; *)
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml () ;
+    ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
     (match current_mml with
       None ->
         let time1 = Sys.time () in