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 echo_error : string -> unit
method echo_message : string -> unit
method wrap_exn : 'a. (unit -> 'a) -> 'a option
+ method choose_uri : string list -> string
+ method show : ?msg:string -> unit -> unit
end
class type disambiguator =
object
- method parserr : parserr
- method setParserr : parserr -> unit
-
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
* 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
- 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
(** 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} *)
type term_source =
[ `Ast of DisambiguateTypes.term
- | `Cic of Cic.term
+ | `Cic of Cic.term * Cic.metasenv
| `String of string
]
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
-