exception No_proof (** no current proof is available *)
+exception Cancel
+exception Unbound_identifier of string
+
+(*
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
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
char Stream.t ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
(** @param env @see disambiguateTerm above *)
method disambiguateTermAst:
?context:Cic.context -> ?metasenv:Cic.metasenv ->
?env:DisambiguateTypes.environment ->
DisambiguateTypes.term ->
- (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
end
(*
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
+ * @return true if no exception has been raised by the evaluation, false
+ * otherwise
+ *)
+ method evalPhrase: string -> bool
+
+ (** as above, evaluating a command/tactics AST *)
+ method evalAst: DisambiguateTypes.tactical -> bool
+
+ (** 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
+
end
(** {2 MathML widgets} *)