X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=95618d142624e932493666da151773b8d9f412c5;hb=06adf83f05c6a4e7acdfc7f590b6ab0d0e18533f;hp=8f59d3fc95276e75ba617364fdd828fa770218f7;hpb=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 8f59d3fc9..95618d142 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -75,6 +75,8 @@ class type console =
     method echo_error     : string -> unit
     method clear          : unit -> unit
     method wrap_exn       : 'a. (unit -> 'a) -> 'a option
+    method choose_uri     : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 type choose_uris_callback =
@@ -137,18 +139,28 @@ 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 =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]