- 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 *)