-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
-
-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
-
- (** schematic representation of items scripts are made of *)
-type script_item =
- [ `Tactic (** action on proof status *)
- | `Theorem (** start of proof, to be proved *)
- | `Qed of UriManager.uri (** end of proof, successfull *)
- | `Def of UriManager.uri (** constant with body *)
- | `Inductive of UriManager.uri (** inductive definition *)
- ]
-
- (** interpreter for toplevel phrases given via console *)
-class type interpreter =
- object
- (** 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
-
- (** {3 callbacks} *)
-
- method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
-
- (** {3 stateful methods}
- * bookkeeping of last interpreted phrase *)
-
- (** 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
-
- (** last item parsed *)
- method lastItem: script_item option
-
- (** change internal interpreter state *)
- method setState: [`Proof | `Command] -> unit
-
- end
-
-(** {2 MathML widgets} *)