diff options
| author | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
| commit | eb7da0d0a02a406c196214ec9d08384385541788 (patch) | |
| tree | efe031d7df32573abd7b39afa0f009a6d61f18d5 /ide | |
| parent | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (diff) | |
| parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 4 | ||||
| -rw-r--r-- | ide/interface.mli | 1 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 4 |
3 files changed, 9 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c28ed68605..1dcef22b91 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -292,11 +292,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; @@ -315,6 +317,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 f3777ba36c..f2f121ac01 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -62,6 +62,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 7445ce5ca0..32c39e20d4 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" |