diff options
| -rw-r--r-- | lib/interface.mli | 16 | ||||
| -rw-r--r-- | lib/serialize.ml | 26 | ||||
| -rw-r--r-- | lib/serialize.mli | 20 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 39 |
4 files changed, 71 insertions, 30 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 *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 41a5f48a6..4846f0153 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -54,6 +54,8 @@ let init_stdout,read_stdout = let r = Buffer.contents out_buff in Buffer.clear out_buff; r) +let pr_debug s = + if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s (** Categories of commands *) @@ -260,11 +262,22 @@ let set_options options = (** Grouping all call handlers together + error handling *) +exception Quit + let eval_call c = let rec handle_exn e = catch_break := false; let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in match e with + | Quit -> + (* Here we do send an acknowledgement message to prove everything went + OK. *) + let dummy = Interface.Good () in + let xml_answer = Serialize.of_answer Serialize.quit dummy in + let () = Xml_utils.print_xml !orig_stdout xml_answer in + let () = flush !orig_stdout in + let () = pr_debug "Exiting gracefully." in + exit 0 | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!" | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner @@ -281,17 +294,18 @@ let eval_call c = r in let handler = { - Interface.interp = interruptible interp; - Interface.rewind = interruptible Backtrack.back; - Interface.goals = interruptible goals; - Interface.evars = interruptible evars; - Interface.hints = interruptible hints; - Interface.status = interruptible status; - Interface.inloadpath = interruptible inloadpath; - Interface.get_options = interruptible get_options; - Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; - Interface.handle_exn = handle_exn; } + Serialize.interp = interruptible interp; + Serialize.rewind = interruptible Backtrack.back; + Serialize.goals = interruptible goals; + Serialize.evars = interruptible evars; + Serialize.hints = interruptible hints; + Serialize.status = interruptible status; + Serialize.inloadpath = interruptible inloadpath; + Serialize.get_options = interruptible get_options; + Serialize.set_options = interruptible set_options; + Serialize.mkcases = interruptible Vernacentries.make_cases; + Serialize.quit = (fun () -> raise Quit); + Serialize.handle_exn = handle_exn; } in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); @@ -307,9 +321,6 @@ let eval_call c = between coqtop and ide. With marshalling, reading an answer to a different request could hang the ide... *) -let pr_debug s = - if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s - let fail err = Serialize.of_value (fun _ -> assert false) (Interface.Fail (None, err)) |