Add command 'Set foo Append "bar"' for appending to an option (bug #5109).

For now, the only meaningful user is "Set Warnings". Example:

Section Bar.
  Local Set Warnings Append "-foo".
  (* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)

6 files changed, 15 insertions, 2 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 9de1df9f1e..680da7f54b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -709,6 +709,7 @@ let rec tmpp v loc =
   | VernacSetStrategy _ as x -> xmlTODO loc x
   | VernacUnsetOption _ as x -> xmlTODO loc x
   | VernacSetOption _ as x -> xmlTODO loc x
+  | VernacSetAppendOption _ as x -> xmlTODO loc x
   | VernacAddOption _ as x -> xmlTODO loc x
   | VernacRemoveOption _ as x -> xmlTODO loc x
   | VernacMemOption _ as x -> xmlTODO loc x
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 279b587831..8572870407 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -429,6 +429,7 @@ type vernac_expr =
       (Conv_oracle.level * reference or_by_notation list) list
   | VernacUnsetOption of Goptions.option_name
   | VernacSetOption of Goptions.option_name * option_value
+  | VernacSetAppendOption of Goptions.option_name * string
   | VernacAddOption of Goptions.option_name * option_ref_value list
   | VernacRemoveOption of Goptions.option_name * option_ref_value list
   | VernacMemOption of Goptions.option_name * option_ref_value list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 50e469dd2a..96eede2b96 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -851,6 +851,8 @@ GEXTEND Gram
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_value ->
   	  VernacSetOption (table,v)
+      | "Set"; table = option_table; "Append"; v = STRING ->
+         VernacSetAppendOption (table,v)
       | "Set"; table = option_table ->
   	  VernacSetOption (table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2d87b51d73..f4a112a4cb 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1110,6 +1110,11 @@ module Make
         return (
           hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
         )
+      | VernacSetAppendOption (na,v) ->
+        return (
+          hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
+                   spc() ++ keyword "Append" ++ spc() ++ str v)
+        )
       | VernacAddOption (na,l) ->
         return (
           hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fa7acd00ab..dc5be08a37 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -181,7 +181,7 @@ let rec classify_vernac e =
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacUnsetOption _ | VernacSetOption _
+    | VernacUnsetOption _ | VernacSetOption _ | VernacSetAppendOption _
     | VernacAddOption _ | VernacRemoveOption _
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2e2a60c861..e16b9128e4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1456,6 +1456,9 @@ let vernac_set_option locality key = function
   | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b
 
+let vernac_set_append_option locality key s =
+  set_string_option_append_value_gen locality key s
+
 let vernac_unset_option locality key =
   unset_option_value_gen locality key
 
@@ -1925,6 +1928,7 @@ let interp ?proof ~loc locality poly c =
   | VernacSetOpacity qidl -> vernac_set_opacity locality qidl
   | VernacSetStrategy l -> vernac_set_strategy locality l
   | VernacSetOption (key,v) -> vernac_set_option locality key v
+  | VernacSetAppendOption (key,v) -> vernac_set_append_option locality key v
   | VernacUnsetOption key -> vernac_unset_option locality key
   | VernacRemoveOption (key,v) -> vernac_remove_option key v
   | VernacAddOption (key,v) -> vernac_add_option key v
@@ -1997,7 +2001,7 @@ let check_vernac_supports_locality c l =
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacSetOption _ | VernacUnsetOption _
+    | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()