X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.ml;h=4f485445d45df0dba5918fab2301fa8bac88e3c8;hb=46008a8be6907e23734a071a1e290ed794e0cae3;hp=98b9cf02c85178f85c71e528759b891075caa07e;hpb=015263908d9142798bcbddbe4c4d13f71e08c5c3;p=helm.git

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 98b9cf02c..4f485445d 100644
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -23,26 +23,51 @@
  * http://helm.cs.unibo.it/
  *)
 
+  (** create a Cic.CurrentProof from a given proof *)
+let currentProof (uri, metasenv, bo, ty) =
+  let uri = MatitaTypes.unopt_uri uri in
+    (* TODO CSC: Wrong: [] is just plainly wrong *)
+  Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+
+let init_metadata status =
+  let ((_, metasenv, _, _) as proof, _) = status in
+  let proof_object_metadata = (* compute proof annotations *)
+    Cic2acic.acic_object_of_cic_object (currentProof proof)
+  in
+  let sequents_metadata = (* compute all sequent annotations from scratch *)
+    List.map
+      (fun ((metano, context, term) as sequent) ->
+        (metano, Cic2acic.asequent_of_sequent metasenv sequent))
+      metasenv
+  in
+  (proof_object_metadata, sequents_metadata)
+
+let compute_metadata (old_status, old_metadata) new_status =
+  let ((_, new_metasenv, _, _) as new_proof, _) = new_status in
+  let proof_object_metadata = (* compute proof annotations *)
+    Cic2acic.acic_object_of_cic_object (currentProof new_proof)
+  in
+  let sequents_metadata = (* compute all sequent annotations from scratch *)
+    (** TODO Zack could we reuse some of the annotations from the previous
+    * status to avoid recomputing all of them? uhm ... we have to which
+    * sequents haven't been changed by last tactic applications ... doh! *)
+    List.map
+      (fun ((metano, context, term) as sequent) ->
+        (metano, Cic2acic.asequent_of_sequent new_metasenv sequent))
+      new_metasenv
+  in
+  (proof_object_metadata, sequents_metadata)
+
 class proof ?uri ~typ ~metasenv ~body () =
   object (self)
 
-    inherit [unit] StatefulProofEngine.status ?uri ~typ ~body ~metasenv
-      (fun _ -> ())
-      (fun _ _ -> ())
-      ()
-
-    method private currentProof =
-      let (uri, metasenv, bo, ty) = self#proof in
-      let uri =
-        match uri with
-        | Some uri -> uri
-        | None -> MatitaTypes.untitled_con_uri
-      in
-        (* TODO CSC: Wrong: [] is just plainly wrong *)
-      Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])
+    inherit [MatitaTypes.hist_metadata]
+      StatefulProofEngine.status
+        ~history_size:BuildTimeConf.history_size ?uri ~typ ~body ~metasenv
+        init_metadata compute_metadata ()
 
     method toXml =
-      let currentproof = self#currentProof in
+      let currentproof = currentProof self#proof in
       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
       in