snapshot, notably:

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

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index ca1b4c9077f9bb32f5af79e0ddf4e5154e224e7e..54ebdf6cf7663340bf5907d433a63ee3f963854c 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -106,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
+