snapshot

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 2811fd5d49ff1f61e0995604a6e13e5c6f8c715e..70f912ae08fd586abe7fad584cdcfb4845010886 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -77,9 +77,18 @@ class type disambiguator =
           (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
   end
 
+type hist_metadata =
+  Cic.annobj *
+  (Cic.id, Cic.term) Hashtbl.t *
+  (Cic.id, Cic.id option) Hashtbl.t *
+  (Cic.id, string) Hashtbl.t *
+  (Cic.id, Cic2acic.anntypes) Hashtbl.t *
+  (Cic.id, Cic.conjecture) Hashtbl.t *
+  (Cic.id, Cic.hypothesis) Hashtbl.t
+
 class type proof =
   object
-    inherit [unit] StatefulProofEngine.status
+    inherit [hist_metadata] StatefulProofEngine.status
 
     (** return a pair of "xml" (as defined in Xml module) representing the *
      * current proof type and body, respectively *)
@@ -113,9 +122,10 @@ type mml_of_cic_sequent =
 
 type mml_of_cic_object =
   explode_all:bool -> UriManager.uri -> Cic.annobj ->
-  (string, string) Hashtbl.t ->
-    (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+  (string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
+    Gdome.document
 
+  (** TODO Zack to be reviewed and unified with proof_viewer above *)
 class type sequent_viewer =
   object
     inherit GMathViewAux.multi_selection_math_view
@@ -138,10 +148,7 @@ class type proof_viewer =
 
       (** @return the annotated cic term and the ids_to_inner_types and
       * ids_to_inner_sorts maps *)
-    method load_proof :
-     UriManager.uri -> Cic.obj ->
-      Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
-       (Cic.id, string) Hashtbl.t
+    method load_proof: Gdome.document -> hist_metadata -> unit
 
   end