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.

8 files changed, 25 insertions, 0 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 94f9c9a36..041f2f83b 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 464e851f6..767c49d2b 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 d337a911d..84fd8929b 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"
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 37218fbf9..9248fa953 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -155,6 +155,7 @@ type option_value = Goptions.option_value =
   | BoolValue of bool
   | IntValue of int option
   | StringValue of string
+  | StringOptValue of string option
 
 type option_ref_value =
   | StringRefValue of string
diff --git a/library/goptions.ml b/library/goptions.ml
index 4f50fbfbd..30d195f83 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -20,6 +20,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 = {
@@ -293,6 +294,10 @@ let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+let declare_stringopt_option =
+  declare_option
+    (fun v -> StringOptValue v)
+    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
@@ -324,11 +329,13 @@ let check_bool_value v = function
 
 let check_string_value v = function
   | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
   | _ -> bad_type_error ()
 
 let check_unset_value v = function
   | BoolValue _ -> BoolValue false
   | IntValue _ -> IntValue None
+  | StringOptValue _ -> StringOptValue None
   | _ -> bad_type_error ()
 
 (* Nota: For compatibility reasons, some errors are treated as
@@ -359,6 +366,8 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
+    | StringOptValue None   -> str"undefined"
+    | StringOptValue (Some s)   -> str s
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
diff --git a/library/goptions.mli b/library/goptions.mli
index 1c44f8908..9d87c14c5 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -128,6 +128,7 @@ type 'a write_function = 'a -> unit
 val declare_int_option   : int option option_sig -> int option write_function
 val declare_bool_option  : bool option_sig   -> bool write_function
 val declare_string_option: string option_sig -> string write_function
+val declare_stringopt_option: string option option_sig -> string option write_function
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -165,6 +166,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/printing/ppvernac.ml b/printing/ppvernac.ml
index 71dcd15cc..76f97fce1 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -166,6 +166,8 @@ module Make
     (* This should not happen because of the grammar *)
       | IntValue (Some n) -> spc() ++ int n
       | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
       | BoolValue b -> mt()
     in pr_printoption a None ++ pr_opt_value b
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c07c756c0..5147d81bc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1497,6 +1497,8 @@ let vernac_set_opacity locality (v,l) =
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen locality key s
+  | StringOptValue None -> unset_option_value_gen locality key
   | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b