added script support a la coqide

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 8f59d3fc95276e75ba617364fdd828fa770218f7..a9e74bf5fdbf1e0bef21d76681dc61481454a85d 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -137,13 +137,23 @@ class type currentProof =
 
 type command_outcome = bool * bool
 
+type script_item =
+  [ `Tactic
+  | `Theorem
+  | `Qed of UriManager.uri
+  | `Def of UriManager.uri
+  | `Inductive of UriManager.uri
+  ]
+
 class type interpreter =
   object
-    method endOffset : int
     method evalAst : DisambiguateTypes.tactical -> command_outcome
     method evalPhrase : string -> command_outcome
 (*     method evalStream: char Stream.t -> command_outcome *)
-    method reset : unit
+    method endOffset : int
+    method lastItem: script_item option
+    method setState: [`Proof | `Command] -> unit
+    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
   end
 
 type term_source =