Merge branch 'v8.6'

4 files changed, 70 insertions, 52 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 813bf30a3..8f2f06925 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -208,6 +208,10 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
+type option_locality = OptLocal | OptDefault | OptGlobal
+
+type option_mod = OptSet | OptAppend
+
 module OptionOrd =
 struct
   type t = option_name
@@ -238,49 +242,51 @@ let warn_deprecated_option =
          (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
                        strbrk " is deprecated")
 
-let declare_option cast uncast
+let get_locality = function
+  | Some true -> OptLocal
+  | Some false -> OptGlobal
+  | None -> OptDefault
+
+let declare_option cast uncast append
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
-  (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
-      That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
-       lists of strings *without* spaces. *)
-  let (write,lwrite,gwrite) = if sync then
-    let ldecl_obj = (* "Local": doesn't survive section or modules. *)
-      declare_object {(default_object ("L  "^nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun _ -> Dispose)}
-    in
-    let decl_obj = (* default locality: survives sections but not modules. *)
-      declare_object {(default_object (nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun _ -> Dispose);
-		       discharge_function = (fun (_,v) -> Some v)}
-    in
-    let gdecl_obj = (* "Global": survives section and modules. *)
-      declare_object {(default_object ("G  "^nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun v -> Substitute v);
-		       subst_function = (fun (_,v) -> v);
-		       discharge_function = (fun (_,v) -> Some v);
-		       load_function = (fun _ (_,v) -> write v)}
-    in
-    let _ = Summary.declare_summary (nickname key)
-	     { Summary.freeze_function = (fun _ -> read ());
-	       Summary.unfreeze_function = write;
-	       Summary.init_function = (fun () -> write default) }
-    in
-    begin fun v -> add_anonymous_leaf (decl_obj v) end ,
-    begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
-    begin fun v -> add_anonymous_leaf (gdecl_obj v) end
-  else write,write,write
+  let change =
+    if sync then
+      let _ = Summary.declare_summary (nickname key)
+        { Summary.freeze_function = (fun _ -> read ());
+          Summary.unfreeze_function = write;
+          Summary.init_function = (fun () -> write default) } in
+      let cache_options (_,(l,m,v)) =
+        match m with
+        | OptSet -> write v
+        | OptAppend -> write (append (read ()) v) in
+      let load_options i o = cache_options o in
+      let subst_options (subst,obj) = obj in
+      let discharge_options (_,(l,_,_ as o)) =
+        match l with OptLocal -> None | _ -> Some o in
+      let classify_options (l,_,_ as o) =
+        match l with OptGlobal -> Substitute o | _ -> Dispose in
+      let options : option_locality * option_mod * _ -> obj =
+        declare_object
+          { (default_object (nickname key)) with
+            load_function = load_options;
+            cache_function = cache_options;
+            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)))
+    else
+      (fun _ m v ->
+       match m with
+       | OptSet -> write v
+       | OptAppend -> write (append (read ()) v))
   in
   let warn () = if depr then warn_deprecated_option key in
   let cread () = cast (read ()) in
-  let cwrite v = warn (); write (uncast v) in
-  let clwrite v = warn (); lwrite (uncast v) in
-  let cgwrite v = warn (); gwrite (uncast v) in
-  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
+  let cwrite l v = warn (); change l OptSet (uncast v) in
+  let cappend l v = warn (); change l OptAppend (uncast v) in
+  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab;
   write
 
 type 'a write_function = 'a -> unit
@@ -289,18 +295,22 @@ let declare_int_option =
   declare_option
     (fun v -> IntValue v)
     (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 let declare_bool_option =
   declare_option
     (fun v -> BoolValue v)
     (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun x y -> x^","^y)
 let declare_stringopt_option =
   declare_option
     (fun v -> StringOptValue v)
     (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
@@ -315,13 +325,8 @@ let set_option_value locality 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,lwrite,gwrite)) ->
-    let write = match locality with
-      | None -> write
-      | Some true -> lwrite
-      | Some false -> gwrite
-    in
-    write (check_and_cast v (read ()))
+  | Some (name, depr, (_,read,write,append)) ->
+    write (get_locality locality) (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option."
 
@@ -357,6 +362,13 @@ let set_string_option_value_gen locality =
 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 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 ()))
+
 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
@@ -375,7 +387,7 @@ let msg_option_value (name,v) =
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
-  let (name, depr, (_,read,_,_,_)) = get_option key in
+  let (name, depr, (_,read,_,_)) = get_option key in
   let s = read () in
   match s with
     | BoolValue b ->
@@ -385,7 +397,7 @@ let print_option_value key =
 
 let get_tables () =
   let tables = !value_tab in
-  let fold key (name, depr, (sync,read,_,_,_)) accu =
+  let fold key (name, depr, (sync,read,_,_)) accu =
     let state = {
       opt_sync = sync;
       opt_name = name;
@@ -404,13 +416,13 @@ let print_tables () =
   in
   str "Synchronous options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (name, depr, (sync,read,_,_,_)) p ->
+      (fun key (name, depr, (sync,read,_,_)) p ->
         if sync then p ++ print_option key name (read ()) depr
         else p)
       !value_tab (mt ()) ++
   str "Asynchronous options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (name, depr, (sync,read,_,_,_)) p ->
+      (fun key (name, depr, (sync,read,_,_)) p ->
         if sync then p
         else p ++ print_option key name (read ()) depr)
       !value_tab (mt ()) ++
diff --git a/library/goptions.mli b/library/goptions.mli
index 26864503b..ca2df0710 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -154,6 +154,7 @@ val get_ref_table :
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
+val set_string_option_append_value_gen : bool option -> option_name -> string -> unit
 val unset_option_value_gen : bool option -> option_name -> unit
 
 val set_int_option_value    : option_name -> int option -> unit
diff --git a/library/lib.ml b/library/lib.ml
index 9401bc55b..4fd29a94d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -234,11 +234,16 @@ let add_leaves id objs =
   List.iter add_obj objs;
   oname
 
-let add_anonymous_leaf obj =
+let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
   let oname = make_oname id in
-  cache_object (oname,obj);
-  add_entry oname (Leaf obj)
+  if cache_first then begin
+    cache_object (oname,obj);
+    add_entry oname (Leaf obj)
+  end else begin
+    add_entry oname (Leaf obj);
+    cache_object (oname,obj)
+  end
 
 let add_frozen_state () =
   add_anonymous_entry
diff --git a/library/lib.mli b/library/lib.mli
index 845727059..9f9d8c7e5 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -54,7 +54,7 @@ val segment_of_objects :
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
-val add_anonymous_leaf : Libobject.obj -> unit
+val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]