- (** @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} *)
-
-type term_source =
- [ `Ast of DisambiguateTypes.term
- | `Cic of Cic.term
- | `String of string
- ]