From 5c995f9bf8408662c23079e19d1b285ef814e8d9 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 25 Nov 2011 18:12:41 +0000 Subject: Added an API call to retrieve and change the option state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14731 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/ide_intf.ml | 168 ++++++++++++++++++++++++++++++++++++++----------- toplevel/ide_intf.mli | 9 +++ toplevel/ide_slave.ml | 15 +++++ toplevel/interface.mli | 16 +++++ 4 files changed, 171 insertions(+), 37 deletions(-) (limited to 'toplevel') diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 29594b140..c702eabb2 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -21,14 +21,20 @@ type 'a call = | Goal | Hints | Status + | GetOptions + | SetOptions of (option_name * option_value) list | InLoadPath of string | MkCases of string +(** The actual calls *) + let interp (r,b,s) : string call = Interp (r,b,s) let rewind i : int call = Rewind i let goals : goals call = Goal let hints : (hint list * hint) option call = Hints let status : status call = Status +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 @@ -42,6 +48,8 @@ let abstract_eval_call handler c = | Goal -> Obj.magic (handler.goals ()) | Hints -> Obj.magic (handler.hints ()) | Status -> Obj.magic (handler.status ()) + | GetOptions -> Obj.magic (handler.get_options ()) + | SetOptions opts -> Obj.magic (handler.set_options opts) | InLoadPath s -> Obj.magic (handler.inloadpath s) | MkCases s -> Obj.magic (handler.mkcases s) in Good res @@ -53,10 +61,22 @@ let abstract_eval_call handler c = exception Marshal_error +(** Utility functions *) + let massoc x l = try List.assoc x l with Not_found -> raise Marshal_error +let constructor t c args = Element (t, ["val", c], args) + +let do_match constr t mf = match constr with +| Element (s, attrs, args) -> + if s = t then + let c = massoc "val" attrs in + mf c args + else raise Marshal_error +| _ -> raise Marshal_error + let pcdata = function | PCData s -> s | _ -> raise Marshal_error @@ -72,19 +92,17 @@ let raw_string = function let bool_arg tag b = if b then [tag, ""] else [] +(** Base types *) + let of_bool b = - if b then Element ("bool", ["val", "true"], []) - else Element ("bool", ["val", "false"], []) + if b then constructor "bool" "true" [] + else constructor "bool" "false" [] -let to_bool = function -| Element ("bool", attrs, []) -> - let ans = massoc "val" attrs in - begin match ans with +let to_bool xml = do_match xml "bool" + (fun s _ -> match s with | "true" -> true | "false" -> false - | _ -> raise Marshal_error - end -| _ -> raise Marshal_error + | _ -> raise Marshal_error) let of_list f l = Element ("list", [], List.map f l) @@ -94,6 +112,69 @@ let to_list f = function List.map f l | _ -> raise Marshal_error +let of_option f = function +| None -> Element ("option", ["val", "none"], []) +| Some x -> Element ("option", ["val", "some"], [f x]) + +let to_option f = function +| Element ("option", ["val", "none"], []) -> None +| Element ("option", ["val", "some"], [x]) -> Some (f x) +| _ -> raise Marshal_error + +let of_string s = Element ("string", [], [PCData s]) + +let to_string = function +| Element ("string", [], l) -> raw_string l +| _ -> raise Marshal_error + +let of_int i = Element ("int", [], [PCData (string_of_int i)]) + +let to_int = function +| Element ("int", [], [PCData s]) -> int_of_string s +| _ -> raise Marshal_error + +let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) + +let to_pair f g = function +| Element ("pair", [], [x; y]) -> (f x, g y) +| _ -> raise Marshal_error + +(** More elaborate types *) + +let of_option_value = function +| IntValue i -> + constructor "option_value" "intvalue" [of_option of_int i] +| BoolValue b -> + constructor "option_value" "boolvalue" [of_bool b] +| StringValue s -> + constructor "option_value" "stringvalue" [of_string s] + +let to_option_value xml = do_match xml "option_value" + (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | _ -> raise Marshal_error + ) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value] + ) + +let to_option_state xml = function +| Element ("option_state", [], [sync; depr; name; value]) -> + { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value; + } +| _ -> raise Marshal_error + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (loc, msg) -> @@ -132,6 +213,11 @@ let of_call = function Element ("call", ["val", "hints"], []) | Status -> Element ("call", ["val", "status"], []) +| GetOptions -> + Element ("call", ["val", "getoptions"], []) +| SetOptions opts -> + let args = List.map (of_pair (of_list of_string) of_option_value) opts in + Element ("call", ["val", "setoptions"], args) | InLoadPath file -> Element ("call", ["val", "inloadpath"], [PCData file]) | MkCases ind -> @@ -150,6 +236,10 @@ let to_call = function Rewind steps | "goal" -> Goal | "status" -> Status + | "getoptions" -> GetOptions + | "setoptions" -> + let args = List.map (to_pair (to_list to_string) to_option_value) l in + SetOptions args | "inloadpath" -> InLoadPath (raw_string l) | "mkcases" -> MkCases (raw_string l) | "hints" -> Hints @@ -157,33 +247,6 @@ let to_call = function end | _ -> raise Marshal_error -let of_option f = function -| None -> Element ("option", ["val", "none"], []) -| Some x -> Element ("option", ["val", "some"], [f x]) - -let to_option f = function -| Element ("option", ["val", "none"], []) -> None -| Element ("option", ["val", "some"], [x]) -> Some (f x) -| _ -> raise Marshal_error - -let of_string s = Element ("string", [], [PCData s]) - -let to_string = function -| Element ("string", [], l) -> raw_string l -| _ -> raise Marshal_error - -let of_int i = Element ("int", [], [PCData (string_of_int i)]) - -let to_int = function -| Element ("int", [], [PCData s]) -> int_of_string s -| _ -> raise Marshal_error - -let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) - -let to_pair f g = function -| Element ("pair", [], [x; y]) -> (f x, g y) -| _ -> raise Marshal_error - let of_status s = let of_so = of_option of_string in Element ("status", [], [of_so s.status_path; of_so s.status_proofname]) @@ -250,6 +313,8 @@ let of_answer (q : 'a call) (r : 'a value) = | Goal -> Obj.magic (of_goals : goals -> xml) | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) | Status -> Obj.magic (of_status : status -> xml) + | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) + | 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) in @@ -259,14 +324,17 @@ let to_answer xml = let rec convert elt = match elt with | Element (tpe, attrs, l) -> begin match tpe with + | "unit" -> Obj.magic () | "string" -> Obj.magic (to_string elt) | "int" -> Obj.magic (to_int elt) - | "goals" -> Obj.magic (to_goals elt) | "status" -> Obj.magic (to_status elt) | "bool" -> Obj.magic (to_bool elt) | "list" -> Obj.magic (to_list convert elt) | "option" -> Obj.magic (to_option convert elt) | "pair" -> Obj.magic (to_pair convert convert elt) + | "goals" -> Obj.magic (to_goals elt) + | "option_value" -> Obj.magic (to_option_value elt) + | "option_state" -> Obj.magic (to_option_state elt) | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -275,6 +343,28 @@ let to_answer xml = (** * Debug printing *) +let pr_option_value = function +| IntValue None -> "none" +| IntValue (Some i) -> string_of_int i +| StringValue s -> s +| BoolValue b -> if b then "true" else "false" + +let rec pr_setoptions opts = + let map (key, v) = + let key = String.concat " " key in + key ^ " := " ^ (pr_option_value v) + in + String.concat "; " (List.map map opts) + +let pr_getoptions opts = + let map (key, s) = + let key = String.concat " " key in + s.opt_name +(* Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s" *) +(* key s.opt_sync s.opt_depr s.opt_name (*(pr_option_value s.opt_value)*) "" *) + in + "\n " ^ String.concat "\n " (List.map map opts) + let pr_call = function | Interp (r,b,s) -> let raw = if r then "RAW" else "" in @@ -284,6 +374,8 @@ let pr_call = function | Goal -> "GOALS" | Hints -> "HINTS" | Status -> "STATUS" + | GetOptions -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" | InLoadPath s -> "INLOADPATH "^s | MkCases s -> "MKCASES "^s @@ -330,5 +422,7 @@ let pr_full_value call value = | Goal -> pr_value_gen pr_goals (Obj.magic value : goals value) | Hints -> pr_value value | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list 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) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index ada6ffe22..9480a7f07 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -51,6 +51,15 @@ val inloadpath : string -> bool call followed by enough pattern variables. *) val mkcases : string -> string list list call +(** Retrieve the list of options of the current toplevel, together with their + state. *) +val get_options : (option_name * option_state) list call + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +val set_options : (option_name * option_value) list -> unit call + 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 76cf15f79..9d0f17ee7 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -472,6 +472,19 @@ let status () = in { Interface.status_path = path; Interface.status_proofname = proof } +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match value with + | BoolValue b -> Goptions.set_bool_option_value name b + | IntValue i -> Goptions.set_int_option_value name i + | StringValue s -> Goptions.set_string_option_value name s + in + List.iter iter options + (** Grouping all call handlers together + error handling *) let eval_call c = @@ -501,6 +514,8 @@ let eval_call c = 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; } in diff --git a/toplevel/interface.mli b/toplevel/interface.mli index b08365e7a..f472929e2 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -32,6 +32,20 @@ type goals = type hint = (string * string) list +type option_name = Goptions.option_name + +type option_value = Goptions.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +type option_state = Goptions.option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + (** * Coq answers to CoqIde *) type location = (int * int) option (* start and end of the error *) @@ -48,6 +62,8 @@ type handler = { goals : unit -> goals; 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; -- cgit v1.2.3