diff options
| author | Gaëtan Gilbert | 2020-02-04 17:07:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 16:23:49 +0100 |
| commit | 4563779bf990cf22d88474a68acf4eb9cfd8d173 (patch) | |
| tree | c5333864070ccc9b8746799e9236ba90ef1a432d /ide/protocol | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
Remove Goptions.opt_name field
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
Diffstat (limited to 'ide/protocol')
| -rw-r--r-- | ide/protocol/interface.ml | 2 | ||||
| -rw-r--r-- | ide/protocol/xmlprotocol.ml | 10 |
2 files changed, 4 insertions, 8 deletions
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index 362833743e..be5e305ad3 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -71,8 +71,6 @@ type option_state = { (** Whether an option is synchronous *) opt_depr : bool; (** Whether an option is deprecated *) - opt_name : string; - (** A short string that is displayed when using [Test] *) opt_value : option_value; (** The current value of the option *) } diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index cad65cc5d6..a2c80ea118 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -79,13 +79,11 @@ 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 = function - | Element ("option_state", [], [sync; depr; name; value]) -> { + | Element ("option_state", [], [sync; depr; value]) -> { opt_sync = to_bool sync; opt_depr = to_bool depr; - opt_name = to_string name; opt_value = to_option_value value } | x -> raise (Marshal_error("option_state",x)) @@ -429,8 +427,8 @@ end = struct | StringOptValue (Some s) -> s | BoolValue b -> if b then "true" else "false" let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" - s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + Printf.sprintf "sync := %b; depr := %b; value := %s\n" + s.opt_sync s.opt_depr (pr_option_value s.opt_value) let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" let pr_coq_object (o : 'a coq_object) = "FIXME" @@ -513,7 +511,7 @@ end = struct "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_name = "name1"; opt_value = IntValue (Some 37) })); + opt_value = IntValue (Some 37) })); end open ReifType |