X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=0f2019ad507b3a3c2d6c9a850ca537001ce3eefd;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=97fa7536a43fb29fb0a76e9ecd93021d45d55b21;hpb=9f62475df3ed7aa7545321d53843cf80281645d7;p=helm.git

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 97fa7536a..0f2019ad5 100644
--- 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;;
 
@@ -124,7 +131,7 @@ 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 ;
@@ -221,15 +228,12 @@ 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