X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaProof.mli;h=9ed6221917d215277b6783435b788bb4ebeb51b9;hb=0d729d0fb3fd7c798382e16c1f855ce26edad979;hp=9293e330afa1c6586fd9d70f90d8be58c2044324;hpb=015263908d9142798bcbddbe4c4d13f71e08c5c3;p=helm.git

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index 9293e330a..9ed622191 100644
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -35,3 +35,25 @@ val proof:
   unit ->
     MatitaTypes.proof
 
+  (** current proof handler *)
+class type currentProof =
+  object
+    inherit MatitaTypes.currentProof
+    
+      (** add an observer to the current observer list. All observers will be
+      * attached to each new proof (method "start") created by this object
+      *)
+    method addObserver: unit StatefulProofEngine.observer -> unit
+
+      (** connect as the first event handler for a given event (abort or quit).
+      * If the event handler returns true, handler processing stops, otherwise
+      * continue with the next handler
+      *)
+    method connect: [`Abort|`Quit] -> (unit -> bool) -> unit
+  end
+
+val currentProof: unit -> currentProof
+
+  (** currentProof singleton instance *)
+val instance: unit -> currentProof
+