1 files changed, 33 insertions, 24 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 5681421ca..76071ebcc 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -196,7 +196,7 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-type option_locality = OptLocal | OptDefault | OptGlobal
+type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
 
 type option_mod = OptSet | OptAppend
 
@@ -229,11 +229,6 @@ let warn_deprecated_option =
          (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
                        strbrk " is deprecated")
 
-let get_locality = function
-  | Some true -> OptLocal
-  | Some false -> OptGlobal
-  | None -> OptDefault
-
 let declare_option cast uncast append ?(preprocess = fun x -> x)
   { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
@@ -247,16 +242,30 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
         match m with
         | OptSet -> write v
         | OptAppend -> write (append (read ()) v) in
-      let load_options i o = cache_options o in
+      let load_options i (_, (l, _, _) as o) = match l with
+      | OptGlobal -> cache_options o
+      | OptExport -> ()
+      | OptLocal | OptDefault ->
+        (** Ruled out by classify_function *)
+        assert false
+      in
+      let open_options i  (_, (l, _, _) as o) = match l with
+      | OptExport -> if Int.equal i 1 then cache_options o
+      | OptGlobal -> ()
+      | OptLocal | OptDefault ->
+        (** Ruled out by classify_function *)
+        assert false
+      in
       let subst_options (subst,obj) = obj in
       let discharge_options (_,(l,_,_ as o)) =
-        match l with OptLocal -> None | _ -> Some o in
+        match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in
       let classify_options (l,_,_ as o) =
-        match l with OptGlobal -> Substitute o | _ -> Dispose in
+        match l with (OptExport | OptGlobal) -> Substitute o | (OptLocal | OptDefault) -> Dispose in
       let options : option_locality * option_mod * _ -> obj =
         declare_object
           { (default_object (nickname key)) with
             load_function = load_options;
+            open_function = open_options;
             cache_function = cache_options;
             subst_function = subst_options;
             discharge_function = discharge_options;
@@ -302,12 +311,12 @@ let warn_unknown_option =
                    (fun key -> strbrk "There is no option " ++
                                  str (nickname key) ++ str ".")
 
-let set_option_value locality check_and_cast key v =
+let set_option_value ?(locality = OptDefault) check_and_cast key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
   | Some (name, depr, (read,write,append)) ->
-    write (get_locality locality) (check_and_cast v (read ()))
+    write locality (check_and_cast v (read ()))
 
 let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
 
@@ -334,25 +343,25 @@ let check_unset_value v = function
    warning. This allows a script to refer to an option that doesn't
    exist anymore *)
 
-let set_int_option_value_gen locality =
-  set_option_value locality check_int_value
-let set_bool_option_value_gen locality key v =
-  set_option_value locality check_bool_value key v
-let set_string_option_value_gen locality =
-  set_option_value locality check_string_value
-let unset_option_value_gen locality key =
-  set_option_value locality check_unset_value key ()
+let set_int_option_value_gen ?locality =
+  set_option_value ?locality check_int_value
+let set_bool_option_value_gen ?locality key v =
+  set_option_value ?locality check_bool_value key v
+let set_string_option_value_gen ?locality =
+  set_option_value ?locality check_string_value
+let unset_option_value_gen ?locality key =
+  set_option_value ?locality check_unset_value key ()
 
-let set_string_option_append_value_gen locality key v =
+let set_string_option_append_value_gen ?(locality = OptDefault) key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
   | Some (name, depr, (read,write,append)) ->
-    append (get_locality locality) (check_string_value v (read ()))
+    append locality (check_string_value v (read ()))
 
-let set_int_option_value = set_int_option_value_gen None
-let set_bool_option_value = set_bool_option_value_gen None
-let set_string_option_value = set_string_option_value_gen None
+let set_int_option_value opt v = set_int_option_value_gen opt v
+let set_bool_option_value opt v = set_bool_option_value_gen opt v
+let set_string_option_value opt v = set_string_option_value_gen opt v
 
 (* Printing options/tables *)