X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=bea4377e6112db7b4802b125d84b9baa072a3d12;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=86e77e7e82ae5d210904a435f12ad4560c6da77d;hpb=3705200c998538c28d8cd9d3ca557616837daf05;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 86e77e7e8..bea4377e6 100644
--- 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} *)