Implement the Export Set/Unset feature.

This feature has been asked many times by different people, and allows to
have options in a module that are performed when this module is imported.

This supersedes the well-numbered cursed PR #313.

1 files changed, 32 insertions, 15 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3610e9da3..7764920d9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1539,13 +1539,17 @@ let vernac_set_opacity ~atts (v,l) =
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
-let get_option_locality = function
-| Some true -> OptLocal
-| Some false -> OptGlobal
-| None -> OptDefault
-
-let vernac_set_option ~atts key opt =
-  let locality = get_option_locality atts.locality in
+let get_option_locality export local =
+  if export then
+    if Option.is_empty local then OptExport
+    else user_err Pp.(str "Locality modifiers forbidden with Export")
+  else match local with
+  | Some true -> OptLocal
+  | Some false -> OptGlobal
+  | None -> OptDefault
+
+let vernac_set_option0 ~atts export key opt =
+  let locality = get_option_locality export atts.locality in
   match opt with
   | StringValue s -> set_string_option_value_gen ~locality key s
   | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
@@ -1553,12 +1557,26 @@ let vernac_set_option ~atts key opt =
   | 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 ~atts key s =
-  let locality = get_option_locality atts.locality in
+let vernac_set_append_option ~atts export key s =
+  let locality = get_option_locality export atts.locality in
   set_string_option_append_value_gen ~locality key s
 
-let vernac_unset_option ~atts key =
-  let locality = get_option_locality atts.locality in
+let vernac_set_option ~atts export table v = match v with
+| StringValue s ->
+  (* We make a special case for warnings because appending is their
+  natural semantics *)
+  if CString.List.equal table ["Warnings"] then
+    vernac_set_append_option ~atts export table s
+  else
+    let (last, prefix) = List.sep_last table in
+    if String.equal last "Append" && not (List.is_empty prefix) then
+      vernac_set_append_option ~atts export prefix s
+    else
+      vernac_set_option0 ~atts export table v
+| _ -> vernac_set_option0 ~atts export table v
+
+let vernac_unset_option ~atts export key =
+  let locality = get_option_locality export atts.locality in
   unset_option_value_gen ~locality key
 
 let vernac_add_option key lv =
@@ -2092,9 +2110,8 @@ let interp ?proof ~atts ~st c =
   | VernacGeneralizable gen -> vernac_generalizable ~atts gen
   | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl
   | VernacSetStrategy l -> vernac_set_strategy ~atts l
-  | VernacSetOption (key,v) -> vernac_set_option ~atts key v
-  | VernacSetAppendOption (key,v) -> vernac_set_append_option ~atts key v
-  | VernacUnsetOption key -> vernac_unset_option ~atts key
+  | VernacSetOption (export, key,v) -> vernac_set_option ~atts export key v
+  | VernacUnsetOption (export, key) -> vernac_unset_option ~atts export key
   | VernacRemoveOption (key,v) -> vernac_remove_option key v
   | VernacAddOption (key,v) -> vernac_add_option key v
   | VernacMemOption (key,v) -> vernac_mem_option key v
@@ -2157,7 +2174,7 @@ let check_vernac_supports_locality c l =
     | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacSetOption _ | VernacSetAppendOption _ | VernacUnsetOption _
+    | VernacSetOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()