X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=864e9604c3d9d853aeaea9c566813b77bc5fdd18;hb=741b3e9014f940fbbd34bee7b606ff7e72170452;hp=27783ec675daab8b6732c9f113b2b3c9f3d6b0b1;hpb=56415e42c04f40e9c8f7cfc59a3a3d87c3d373f7;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 27783ec67..864e9604c 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -64,10 +64,7 @@ class type command =
 class type parserr =  (* "parser" is a keyword :-( *)
   object
     method parseTerm:     char Stream.t -> DisambiguateTypes.term
-    method parseTactic:   char Stream.t -> DisambiguateTypes.tactic
     method parseTactical: char Stream.t -> DisambiguateTypes.tactical
-    method parseCommand:  char Stream.t -> DisambiguateTypes.command
-    method parseScript:   char Stream.t -> DisambiguateTypes.script
   end
 
 class type disambiguator =
@@ -129,6 +126,15 @@ class type proof =
     method setStatus: proofStatus -> unit
   end
 
+type proof_handler =
+  { get_proof: unit -> proof; (* return current proof or fail *)
+    set_proof: proof option -> unit;  (* set a proof option as current proof *)
+    has_proof: unit -> bool;  (* check if a current proof is available or not *)
+    new_proof: proof -> unit; (* as a set_proof but takes care also to register
+                              observers *)
+    quit: unit -> unit
+  }
+
   (** interpreter for toplevel phrases given via console *)
 class type interpreter =
   object