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
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
+ * 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
(*
- (** 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
+ (** undo last steps phrases.
+ * @param steps number of phrases to undo; defaults to 1 *)
+ method undo: ?steps:int -> unit -> unit
*)
+
end
(** {2 MathML widgets} *)