-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
-
- (** {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
-
-(** {2 major matita objects} *)
-
-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 env : DisambiguateTypes.environment
- method setEnv : DisambiguateTypes.environment -> unit
-
- method chooseUris: choose_uris_callback
- method setChooseUris: choose_uris_callback -> unit
-
- method chooseInterp: choose_interp_callback
- method setChooseInterp: choose_interp_callback -> unit
-
- method parserr: parserr
-
- (* 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