summaryrefslogtreecommitdiff
path: root/ide/xmlprotocol.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
commit4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch)
treeaefad2e3de35f75c46729f9310d33b56d3821961 /ide/xmlprotocol.ml
parent64fa31c7ee53e79b112507fb2eea27dc7648328d (diff)
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'ide/xmlprotocol.ml')
-rw-r--r--ide/xmlprotocol.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d337a911..84fd8929 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"