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"
| 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
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} *)