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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 86e77e7e8..20ffd350d 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -35,6 +35,9 @@ let debug_print s =
 
 exception No_proof  (** no current proof is available *)
 
+exception Cancel
+
+(*
 let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
 let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
 
@@ -42,6 +45,8 @@ let unopt_uri ?(kind = `Con) = function
   | Some uri -> uri
   | None ->
       (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
+*)
+let unopt_uri = function Some uri -> uri | None -> assert false
 
 class type parserr =  (* "parser" is a keyword :-( *)
   object
@@ -121,7 +126,26 @@ type proof_handler =
 class type interpreter =
   object
     method reset: unit  (** return the interpreter to the initial state *)
-    method evalPhrase: string -> unit
+
+      (** parse a single phrase contained in the input string. Additional
+      * garbage at the end of the phrase is ignored
+      * @param transparent per default the interpreter catch all exceptions ans
+      * prints them in the console. When transparent is set to true exceptions
+      * are flow through. Defaults to false
+      *)
+    method evalPhrase: ?transparent:bool -> string -> unit
+
+      (** 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
+
+(*
+      (** undo last steps phrases.
+      * @param steps number of phrases to undo; defaults to 1 *)
+    method undo: ?steps:int -> unit -> unit
+*)
+
   end
 
 (** {2 MathML widgets} *)