-exception Statement_error of string
-val statement_error : string -> 'a
-
-exception Command_error of string
-val command_error : string -> 'a
-
-exception Option_error of string * string
-exception Unbound_identifier of string
-
-type proof_status =
- No_proof
- | Incomplete_proof of ProofEngineTypes.status
- | Proof of ProofEngineTypes.proof
- | Intermediate of Cic.metasenv
-
-module StringMap : Map.S with type key = String.t
-
-type option_value =
- | String of string
- | Int of int
-type options = option_value StringMap.t
-val no_options : 'a StringMap.t
-
-type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
-
-type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: moo;
- proof_status: proof_status; (** logical status *)
- options: options;
- objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
- notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
-}
-
-val set_metasenv: Cic.metasenv -> status -> status
-
- (** list is not reversed, head command will be the first emitted *)
-val add_moo_content: ast_command list -> status -> status
-val add_moo_metadata: GrafiteAst.metadata list -> status -> status
-
-val dump_status : status -> unit
-val get_option : status -> StringMap.key -> option_value
-val get_string_option : status -> StringMap.key -> string
-val set_option : status -> StringMap.key -> string -> status
-
-class type console =
- object
- method choose_uri : string list -> string
- method clear : unit -> unit
- method echo_error : string -> unit
- method echo_message : string -> unit
- method show : ?msg:string -> unit -> unit
- method wrap_exn : (unit -> 'a) -> 'a option
- end