aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorEnrico Tassi2015-10-06 14:11:19 +0200
committerEnrico Tassi2015-10-08 09:51:13 +0200
commitce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 (patch)
treef37a9f9b4aadcd6b07fce72885f879d457ab78dd /ide
parent27d4a636cb7f1fbdbced1980808a9b947405eeb5 (diff)
Goptions: new value type: optional string
These options can be set to a string value, but also unset. Internal data is of type string option.
Diffstat (limited to 'ide')
-rw-r--r--ide/ide_slave.ml4
-rw-r--r--ide/interface.mli1
-rw-r--r--ide/xmlprotocol.ml4
3 files changed, 9 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a361..041f2f83b8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -291,11 +291,13 @@ let export_option_value = function
| Goptions.BoolValue b -> Interface.BoolValue b
| Goptions.IntValue x -> Interface.IntValue x
| Goptions.StringValue s -> Interface.StringValue s
+ | Goptions.StringOptValue s -> Interface.StringOptValue s
let import_option_value = function
| Interface.BoolValue b -> Goptions.BoolValue b
| Interface.IntValue x -> Goptions.IntValue x
| Interface.StringValue s -> Goptions.StringValue s
+ | Interface.StringOptValue s -> Goptions.StringOptValue s
let export_option_state s = {
Interface.opt_sync = s.Goptions.opt_sync;
@@ -314,6 +316,8 @@ let set_options options =
| 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
+ | StringOptValue (Some s) -> Goptions.set_string_option_value name s
+ | StringOptValue None -> Goptions.unset_option_value_gen None name
in
List.iter iter options
diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..767c49d2bd 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -61,6 +61,7 @@ type option_value =
| BoolValue of bool
| IntValue of int option
| StringValue of string
+ | StringOptValue of string option
(** Summary of an option status *)
type option_state = {
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911d8..84fd8929bd 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -62,10 +62,12 @@ 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]
+ | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s]
let to_option_value = do_match "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))
+ | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args))
| _ -> raise Marshal_error)
let of_option_state s =
@@ -337,6 +339,8 @@ end = struct
| IntValue None -> "none"
| IntValue (Some i) -> string_of_int i
| StringValue s -> s
+ | StringOptValue None -> "none"
+ | 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"