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

3 files changed, 46 insertions, 16 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index f2aba72e9..a72e5b7b0 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -75,19 +75,3 @@ type location = (int * int) option (* start and end of the error *)
 type 'a value =
   | Good of 'a
   | Fail of (location * string)
-
-(** * 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;
-  handle_exn : exn -> location * string;
-}
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 96cdc6c2c..3b4386131 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -27,6 +27,24 @@ type 'a call =
   | SetOptions of (option_name * option_value) list
   | InLoadPath of string
   | MkCases of string
+  | Quit
+
+(** 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;
+}
 
 (** The actual calls *)
 
@@ -40,6 +58,7 @@ let get_options : (option_name * option_state) list call = GetOptions
 let set_options l : unit call = SetOptions l
 let inloadpath s : bool call = InLoadPath s
 let mkcases s : string list list call = MkCases s
+let quit : unit call = Quit
 
 (** * Coq answers to CoqIde *)
 
@@ -56,6 +75,7 @@ let abstract_eval_call handler c =
       | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
       | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
       | MkCases s -> Obj.magic (handler.mkcases s : string list list)
+      | Quit -> Obj.magic (handler.quit () : unit)
     in Good res
   with e ->
     let (l, str) = handler.handle_exn e in
@@ -228,6 +248,8 @@ let of_call = function
   Element ("call", ["val", "inloadpath"], [PCData file])
 | MkCases ind ->
   Element ("call", ["val", "mkcases"], [PCData ind])
+| Quit ->
+  Element ("call", ["val", "quit"], [])
 
 let to_call = function
 | Element ("call", attrs, l) ->
@@ -250,6 +272,7 @@ let to_call = function
   | "inloadpath" -> InLoadPath (raw_string l)
   | "mkcases" -> MkCases (raw_string l)
   | "hints" -> Hints
+  | "quit" -> Quit
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -325,6 +348,7 @@ let of_answer (q : 'a call) (r : 'a value) =
   | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
   | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
   | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
+  | Quit -> Obj.magic (fun _ -> Element ("unit", [], []))
   in
   of_value convert r
 
@@ -387,6 +411,7 @@ let pr_call = function
   | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
   | InLoadPath s -> "INLOADPATH "^s
   | MkCases s -> "MKCASES "^s
+  | Quit -> "QUIT"
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
@@ -445,3 +470,4 @@ let pr_full_value call value =
     | SetOptions _ -> pr_value value
     | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
     | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
+    | Quit -> pr_value value
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 *)