diff options
Diffstat (limited to 'lib/serialize.ml')
| -rw-r--r-- | lib/serialize.ml | 26 |
1 files changed, 26 insertions, 0 deletions
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 |