class type parserr = (* "parser" is a keyword :-( *)
object
method parseTerm: char Stream.t -> DisambiguateTypes.term
- method parseTactic: char Stream.t -> DisambiguateTypes.tactic
method parseTactical: char Stream.t -> DisambiguateTypes.tactical
- method parseCommand: char Stream.t -> DisambiguateTypes.command
- method parseScript: char Stream.t -> DisambiguateTypes.script
end
class type disambiguator =
method setStatus: proofStatus -> unit
end
+type proof_handler =
+ { get_proof: unit -> proof; (* return current proof or fail *)
+ set_proof: proof option -> unit; (* set a proof option as current proof *)
+ has_proof: unit -> bool; (* check if a current proof is available or not *)
+ new_proof: proof -> unit; (* as a set_proof but takes care also to register
+ observers *)
+ quit: unit -> unit
+ }
+
(** interpreter for toplevel phrases given via console *)
class type interpreter =
object