Added an interface call to exit Coqtop nicely.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/lib/serialize.mli b/lib/serialize.mli
index 2ab557c53..6407276ba 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -67,6 +67,26 @@ val get_options : (option_name * option_state) list call
     to check that everything is correct. *)
 val set_options : (option_name * option_value) list -> unit call
 
+(** Quit gracefully the interpreter. *)
+val quit : unit call
+
+(** The structure that coqtop should implement *)
+
+type handler = {
+  interp : raw * verbose * string -> string;
+  rewind : int -> int;
+  goals : unit -> goals option;
+  evars : unit -> evar list option;
+  hints : unit -> (hint list * hint) option;
+  status : unit -> status;
+  get_options : unit -> (option_name * option_state) list;
+  set_options : (option_name * option_value) list -> unit;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
+  quit : unit -> unit;
+  handle_exn : exn -> location * string;
+}
+
 val abstract_eval_call : handler -> 'a call -> 'a value
 
 (** * XML data marshalling *)