diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 1 | ||||
| -rw-r--r-- | ide/protocol/interface.ml | 2 | ||||
| -rw-r--r-- | ide/protocol/xmlprotocol.ml | 10 |
3 files changed, 4 insertions, 9 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 7d92cff365..ae2301a0a7 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -360,7 +360,6 @@ let import_option_value = function let export_option_state s = { Interface.opt_sync = true; Interface.opt_depr = s.Goptions.opt_depr; - Interface.opt_name = s.Goptions.opt_name; Interface.opt_value = export_option_value s.Goptions.opt_value; } 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 |