diff options
| author | Enrico Tassi | 2015-10-06 14:11:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-10-08 09:51:13 +0200 |
| commit | ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 (patch) | |
| tree | f37a9f9b4aadcd6b07fce72885f879d457ab78dd /ide/xmlprotocol.ml | |
| parent | 27d4a636cb7f1fbdbced1980808a9b947405eeb5 (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/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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" |
