*)
exception Cancel
-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 status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- moo_content_rev: string list;(*CSC: GrafiteAst.command list would be better *)
- proof_status: proof_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
-
-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
type abouts = [ `Blank | `Current_proof | `Us ]
| `Uri of UriManager.uri
| `Whelp of string * UriManager.uri list ]
-val string_of_entry :
- [< `About of [< `Blank | `Current_proof | `Us ]
- | `Check of 'a
- | `Cic of 'b * 'c
- | `Dir of string
- | `Uri of UriManager.uri
- | `Whelp of string * 'd ] ->
- string
-
-val entry_of_string :
- string -> [> `About of [> `Blank | `Current_proof | `Us ] ]
+val string_of_entry : mathViewer_entry -> string
+val entry_of_string : string -> mathViewer_entry
class type mathViewer =
object