From 7ba82ed9f595c7d93bd40846993c2447572a817a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Nov 2016 15:54:37 +0100
Subject: Put string between quotes when printing an option value.

This is a better (more generic) fix to #5061 than my e8b9ee76.
---
 library/goptions.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index 35616558a6..dfb3c0e698 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -381,9 +381,9 @@ let msg_option_value (name,v) =
     | BoolValue false -> str "off"
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
-    | StringValue s   -> str s
+    | StringValue s   -> str "\"" ++ str s ++ str "\""
     | StringOptValue None   -> str"undefined"
-    | StringOptValue (Some s)   -> str s
+    | StringOptValue (Some s)   -> str "\"" ++ str s ++ str "\""
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
-- 
cgit v1.2.3


From 2c5eef988f11979175de6d1983bc533ce18b1095 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Nov 2016 15:57:19 +0100
Subject: Fix various shortcomings of the warnings infrastructure.

- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
---
 library/goptions.ml  |  7 ++++---
 library/goptions.mli | 14 ++++++++++----
 2 files changed, 14 insertions(+), 7 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index dfb3c0e698..9dc0f40588 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -247,7 +247,7 @@ let get_locality = function
   | Some false -> OptGlobal
   | None -> OptDefault
 
-let declare_option cast uncast append
+let declare_option cast uncast append ?(preprocess = fun x -> x)
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
@@ -275,10 +275,11 @@ let declare_option cast uncast append
             subst_function = subst_options;
             discharge_function = discharge_options;
             classify_function = classify_options } in
-      (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v)))
+      (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
     else
       (fun _ m v ->
-       match m with
+        let v = preprocess v in
+        match m with
        | OptSet -> write v
        | OptAppend -> write (append (read ()) v))
   in
diff --git a/library/goptions.mli b/library/goptions.mli
index ca2df07104..3b3651f393 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -122,13 +122,19 @@ type 'a option_sig = {
 
 (** When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
+(** The [preprocess] function is triggered before setting the option. It can be
+    used to emit a warning on certain values, and clean-up the final value. *)
 
 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
+val declare_int_option   : ?preprocess:(int option -> int option) ->
+                           int option option_sig -> int option write_function
+val declare_bool_option  : ?preprocess:(bool -> bool) ->
+                           bool option_sig   -> bool write_function
+val declare_string_option: ?preprocess:(string -> string) ->
+                           string option_sig -> string write_function
+val declare_stringopt_option: ?preprocess:(string option -> string option) ->
+                              string option option_sig -> string option write_function
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
-- 
cgit v1.2.3