X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.ml;h=54ebdf6cf7663340bf5907d433a63ee3f963854c;hb=ac813b7e251e4bac1a8a16befa628203775771ca;hp=17b44ffd3ee600ca79af6e2d7d123c2fd01ef7b6;hpb=06c2b37f3d7d4e14cabeef3b18211e5d12b9b4eb;p=helm.git

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 17b44ffd3..54ebdf6cf 100644
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -23,25 +23,57 @@
  * 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, [])
+open MatitaCicMisc
+
+let init_metadata _ = ()
+let compute_metadata _ _ = ()
+
+(*
+let init_metadata status =
+  let ((_, metasenv, _, _) as proof, _) = status in
+  let proof_object_metadata = (* compute proof annotations *)
+    Cic2acic.acic_object_of_cic_object (cicCurrentProof 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, goal_opt) = new_status in
+  let proof_object_metadata = (* compute proof annotations *)
+    let obj =
+      match goal_opt with
+      | Some _ -> cicCurrentProof new_proof
+      | None -> cicConstant new_proof
+    in
+    Cic2acic.acic_object_of_cic_object obj
+  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 [MatitaTypes.hist_metadata]
-      StatefulProofEngine.status ?uri ~typ ~body ~metasenv
-        (fun proof ->
-          Cic2acic.acic_object_of_cic_object (currentProof (fst proof)))
-        (fun (old_proof, old_metadata) new_proof ->
-          Cic2acic.acic_object_of_cic_object (currentProof (fst new_proof)))
-        ()
+    inherit [unit]
+      StatefulProofEngine.status
+        ~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv
+        init_metadata compute_metadata ()
 
     method toXml =
-      let currentproof = currentProof self#proof in
+      let currentproof = cicCurrentProof self#proof in
       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
       in
@@ -74,9 +106,49 @@ class proof ?uri ~typ ~metasenv ~body () =
 
   end
 
+class currentProof =
+  let fail () = failwith "No current proof" in
+  object (self)
+    val mutable _proof: MatitaTypes.proof option = None
+    val mutable observers = []
+    val mutable callbacks = []
+
+    initializer self#connect `Abort (fun () -> _proof <- None; false)
+
+      (** execute all callbacks related to a given event until one of them
+      * return true or the end of the callback list is reached *)
+    method private do_callbacks event =
+      let rec aux = function
+        | [] -> ()
+        | (event', f) :: tl when event' = event -> if not (f ()) then aux tl
+        | _ :: tl -> aux tl
+      in
+      aux callbacks
+
+    method addObserver o = observers <- o :: observers
+
+    method connect (event:[`Abort|`Quit]) f =
+      callbacks <- (event, f) :: callbacks
+
+    method onGoing () = _proof <> None
+    method proof = match _proof with None -> fail () | Some proof -> proof
+    method start (proof: MatitaTypes.proof) =
+      List.iter
+        (fun observer ->
+          ignore (proof#attach_observer
+            ~interested_in:StatefulProofEngine.all_events observer))
+        observers;
+      proof#notify;
+      _proof <- Some proof
+    method abort () = self#do_callbacks `Abort
+    method quit () = self#do_callbacks `Quit
+  end
+
 let proof ?uri ~metasenv ~typ () =
   let metasenv = (1, [], typ) :: metasenv in
   let body = Cic.Meta (1,[]) in
   let _  = CicTypeChecker.type_of_aux' metasenv [] typ in
   new proof ~typ ~metasenv ~body ?uri ()
 
+let currentProof () = new currentProof
+