debian version 0.0.5-6

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 99e69f6e1cb5e7a0de251fdb419ca5c105be9a23..26299967224cb6b4f850da5a53935360691296e9 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -72,6 +72,8 @@ class type console =
     method echo_error : string -> unit
     method echo_message : string -> unit
     method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 class type disambiguator =
@@ -146,11 +148,18 @@ class type currentProof =
   * second component represents console action: true = hide, false = keep *)
 type command_outcome = bool * bool
 
+  (** schematic representation of items scripts are made of *)
+type script_item =
+  [ `Tactic                       (** action on proof status *)
+  | `Theorem                      (** start of proof, to be proved *)
+  | `Qed of UriManager.uri        (** end of proof, successfull *)
+  | `Def of UriManager.uri        (** constant with body *)
+  | `Inductive of UriManager.uri  (** inductive definition *)
+  ]
+
   (** interpreter for toplevel phrases given via console *)
 class type interpreter =
   object
-    method reset: unit  (** return the interpreter to the initial state *)
-
       (** parse a single phrase contained in the input string. Additional
       * garbage at the end of the phrase is ignored
       * @return true if no exception has been raised by the evaluation, false
@@ -165,18 +174,31 @@ class type interpreter =
       (** as above, evaluating a command/tactics AST *)
     method evalAst: DisambiguateTypes.tactical -> command_outcome
 
+    (** {3 callbacks} *)
+
+    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
+
+    (** {3 stateful methods}
+     * bookkeeping of last interpreted phrase *)
+
       (** offset from the starting of the last string parser by evalPhrase where
       * parsing stop.
       * @raise Failure when no offset has been recorded *)
     method endOffset: int
 
+      (** last item parsed *)
+    method lastItem: script_item option
+
+      (** change internal interpreter state *)
+    method setState: [`Proof | `Command] -> unit
+
   end
 
 (** {2 MathML widgets} *)
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]