*)
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 incomplete_proof = {
- proof: ProofEngineTypes.proof;
- stack: Continuationals.Stack.t;
-}
-
-type proof_status =
- No_proof
- | Incomplete_proof of incomplete_proof
- | 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, CicNotationPt.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 *)
- coercions: UriManager.uri list; (** defined coercions *)
- 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
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
method show_uri_list :
?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
end
-
-val qualify: status -> string -> string
-
-val get_current_proof: status -> ProofEngineTypes.proof
-val get_proof_metasenv: status -> Cic.metasenv
-val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context
-val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
-val get_stack: status -> Continuationals.Stack.t
-
-val set_stack: Continuationals.Stack.t -> status -> status
-