+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** exceptions whose content should be presented to the user *)
+exception Not_implemented of string
+exception Failure of string
+
+val not_implemented : string -> 'a
+val error : string -> 'a
+val warning : string -> unit
+val debug_print : string -> unit
+
+exception No_proof (** no current proof is available *)
+exception Cancel
+exception Unbound_identifier of string
+
+ (** @param exn an exception
+ * @return a string which is meant to be a textual explaination of the
+ exception understandable by a user *)
+val explain: exn -> string
+
+val unopt_uri : 'a option -> 'a
+
+class type parserr =
+ object
+ method parseTactical : char Stream.t -> DisambiguateTypes.tactical
+ method parseTerm : char Stream.t -> DisambiguateTypes.term
+ end
+
+ (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
+ object
+ method clear : unit -> unit
+ method echo_error : string -> unit
+ method echo_message : string -> unit
+ method wrap_exn : 'a. (unit -> 'a) -> 'a option
+ end
+
+class type disambiguator =
+ object
+ method parserr : parserr
+ method setParserr : parserr -> unit
+
+ method env : DisambiguateTypes.environment
+ method setEnv : DisambiguateTypes.environment -> unit
+
+ (* TODO Zack: as long as matita doesn't support MDI inteface,
+ * disambiguateTerm will return a single term *)
+ (** @param env disambiguation environment. If this parameter is given the
+ * disambiguator act statelessly, that is internal disambiguation status
+ * want be changed but only returned. If this parameter is not given the
+ * internal one will be used and updated with the disambiguation status
+ * resulting from the disambiguation *)
+ method disambiguateTerm :
+ ?context:Cic.context ->
+ ?metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ char Stream.t ->
+ 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 *
+ CicUniv.universe_graph
+
+ (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
+ * AST should be closed hence no context param is permitted on this method
+ *)
+ method disambiguateTermAsts :
+ ?metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ DisambiguateTypes.term list ->
+ DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
+ CicUniv.universe_graph
+ end
+
+class type proof =
+ object
+ inherit [unit] StatefulProofEngine.status
+
+ (** return a pair of "xml" (as defined in Xml module) representing the *
+ * current proof type and body, respectively *)
+ method toXml : Xml.token Stream.t * Xml.token Stream.t
+
+ method toString : string
+ end
+
+class type currentProof =
+ object
+ method onGoing: unit -> bool (** true if a proof is on going *)
+ method proof: proof (** @raise Failure "No current proof" *)
+ method start: proof -> unit (** starts a new proof *)
+ method abort: unit -> unit (** abort the on going proof *)
+ method quit: unit -> unit (** quit matita *)
+ end
+
+ (** first component represents success: true = success, false = failure
+ * second component represents console action: true = hide, false = keep *)
+type command_outcome = bool * bool
+
+ (** interpreter for toplevel phrases given via console *)
+class type interpreter =
+ 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
+ * @return true if no exception has been raised by the evaluation, false
+ * otherwise
+ *)
+ method evalPhrase: string -> command_outcome
+
+ (** as evalPhrase above, but parses a character stream. Only characters
+ * composing next phrases are consumed *)
+(* method evalStream: char Stream.t -> command_outcome *)
+
+ (** as above, evaluating a command/tactics AST *)
+ method evalAst: DisambiguateTypes.tactical -> command_outcome
+
+ (** 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} *)
+
+class type mathViewer =
+ object
+ method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
+ method unload: unit -> unit
+ end
+
+type mml_of_cic_sequent =
+ Cic.metasenv ->
+ Cic.conjecture ->
+ Gdome.document *
+ ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t)
+
+type mml_of_cic_object =
+ explode_all:bool ->
+ UriManager.uri ->
+ Cic.annobj ->
+ (string, string) Hashtbl.t ->
+ (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+
+(** {2 shorthands} *)
+
+type namer = ProofEngineTypes.mk_fresh_name_type
+
+ (** {3 disambiguator callbacks} *)
+
+type choose_uris_callback =
+ selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?title:string ->
+ ?msg:string -> ?nonvars_button:bool -> string list -> string list
+
+type choose_interp_callback = (string * string) list list -> int list
+
+ (** @raise Failure if called, use if unambiguous input is required *)
+val mono_uris_callback: choose_uris_callback
+ (** @raise Failure if called, use if unambiguous input is required *)
+val mono_interp_callback: choose_interp_callback
+