snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 86e77e7e82ae5d210904a435f12ad4560c6da77d..bea4377e6112db7b4802b125d84b9baa072a3d12 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -121,7 +121,19 @@ type proof_handler =
 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 *)
     method evalPhrase: string -> unit
+
+(*
+      (** eval zero or more phrases contained in the input string. Additional
+      * garbage contained at the end of the last phrase is ignored.
+      * @return offset from the beginning of the string pointing to the end of
+      * the last parsed phrase. Next invocations of evalAll should start from
+      * there *)
+    method evalAll: string -> int
+*)
   end
 
 (** {2 MathML widgets} *)