Ajout de la gestion de Local et Global pour les options (au sens de

Goptions).
- Local Set/Unset ... change la valeur de l'option pour la section en
cours (ou le module si il n'y a pas de section), l'option est restaurée
à sa valeur précédente au sortir de la section.
- Set/Unset ... survit aux sections mais pas aux modules.
- Global Set/Unset ... survit aux sections et aux modules.

Il y a une légère source d'incompatibilité là, Set avait le comportement
de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on
jamais.

Les étapes suivantes :
- Supprimer la notion d'option asynchrone, je n'en vois vraiment pas
l'intérêt. Changer le type de retour de declare_option à unit aussi
serait probablement une bonne idée.
- Ajouter le support Local/Global à d'autres commandes sur le même
modèle.

Conflicts:

	parsing/g_vernac.ml4


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 87 insertions, 49 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 35feb59ed..4fd48a306 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -275,8 +275,8 @@ let rec attribute_of_vernac_command = function
   | VernacDeclareImplicits _ -> []
   | VernacReserve _ -> []
   | VernacSetOpacity _ -> []
-  | VernacSetOption (["Ltac";"Debug"], _) -> [DebugCommand]
-  | VernacSetOption (o,BoolValue true) | VernacUnsetOption o ->
+  | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
+  | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
       if coqide_known_option o then [KnownOptionCommand] else []
   | VernacSetOption _ -> []
   | VernacRemoveOption _ -> []
diff --git a/library/goptions.ml b/library/goptions.ml
index bf431e1fc..86012b113 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -235,24 +235,46 @@ let declare_option cast uncast
   { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
-  let write = if sync then 
-    let (decl_obj,_) = 
-      declare_object {(default_object (nickname key)) with
+  (* 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 -> Keep v);
+		       discharge_function = (fun (_,v) -> Some v);
+		       load_function = (fun _ (_,v) -> write v);
+		       (* spiwack: I'm unsure whether this function does anyting *)
+		       export_function = (fun v -> Some v)}
+    in 
     let _ = declare_summary (nickname key) 
 	     { freeze_function = read;
 	       unfreeze_function = write;
 	       init_function = (fun () -> write default) }
     in 
-    fun v -> add_anonymous_leaf (decl_obj v)
-  else write
+    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
   in 
   let cread () = cast (read ()) in
   let cwrite v = write (uncast v) in 
-  value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; 
-  write
+  let clwrite v = lwrite (uncast v) in 
+  let cgwrite v = gwrite (uncast v) in 
+  value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab; 
+  write 
 
 type 'a write_function = 'a -> unit
 
@@ -273,28 +295,37 @@ let declare_string_option =
 
 (* Setting values of options *)
 
-let set_option_value check_and_cast key v =
-  let (name,(_,read,write)) =
+let set_option_value locality check_and_cast key v =
+  let (name,(_,read,write,lwrite,gwrite)) =
     try get_option key
     with Not_found -> error ("There is no option "^(nickname key)^".")
   in
+  let write = match locality with
+    | None -> write
+    | Some true -> lwrite
+    | Some false -> gwrite
+  in
   write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option"
 
-let set_int_option_value = set_option_value
+let set_int_option_value_gen locality = set_option_value  locality
   (fun v -> function 
      | (IntValue _) -> IntValue v
      | _ -> bad_type_error ())
-let set_bool_option_value = set_option_value
+let set_bool_option_value_gen locality = set_option_value locality
   (fun v -> function 
      | (BoolValue _) -> BoolValue v
      | _ -> bad_type_error ())
-let set_string_option_value = set_option_value
+let set_string_option_value_gen locality = set_option_value locality
  (fun v -> function 
     | (StringValue _) -> StringValue v
     | _ -> bad_type_error ())
 
+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
+
 (* Printing options/tables *)
 
 let msg_option_value (name,v) =
@@ -307,7 +338,7 @@ let msg_option_value (name,v) =
     | IdentValue r    -> pr_global_env Idset.empty r
 
 let print_option_value key =
-  let (name,(_,read,_)) = get_option key in
+  let (name,(_,read,_,_,_)) = get_option key in
   let s = read () in 
   match s with
     | BoolValue b -> 
@@ -322,7 +353,7 @@ let print_tables () =
   msg
     (str "Synchronous options:" ++ fnl () ++
      OptionMap.fold 
-       (fun key (name,(sync,read,write)) p -> 
+       (fun key (name,(sync,read,_,_,_)) p -> 
 	  if sync then 
 	    p ++ str ("  "^(nickname key)^": ") ++
 	    msg_option_value (name,read()) ++ fnl ()
@@ -331,7 +362,7 @@ let print_tables () =
        !value_tab (mt ()) ++
      str "Asynchronous options:" ++ fnl () ++
      OptionMap.fold 
-       (fun key (name,(sync,read,write)) p -> 
+       (fun key (name,(sync,read,_,_,_)) p -> 
 	  if sync then 
 	    p
 	  else 
diff --git a/library/goptions.mli b/library/goptions.mli
index aefddbbda..eba44a896 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -153,6 +153,11 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
+(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+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_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
 val set_string_option_value : option_name -> string -> unit
diff --git a/library/libobject.mli b/library/libobject.mli
index f32d3baa7..a8b5702f8 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -29,7 +29,7 @@ open Mod_subst
    * an opening function, specifying what to do when the module 
      containing the object is opened (imported);
      If the object wishes to register its visibility in the Nametab, 
-     it should do so for the sufix of the length the "int" argument
+     it should do so for the suffix of the length the "int" argument
 
    * a classification function, specyfying what to do with the object,
      when the current module (containing the object) is ended;
@@ -49,7 +49,7 @@ open Mod_subst
 
    * a substitution function, performing the substitution; 
      this function should be declared for substitutive objects 
-     only (see obove)
+     only (see above)
 
    * a discharge function, that is applied at section closing time to
      collect the data necessary to rebuild the discharged form of the
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ea686e5a3..d10a2950c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -637,11 +637,11 @@ GEXTEND Gram
 
       (* Pour intervenir sur les tables de param��tres *)
       | "Set"; table = option_table; v = option_value ->
-  	  VernacSetOption (table,v)
+  	  VernacSetOption (use_locality_full(),table,v)
       | "Set"; table = option_table ->
-  	  VernacSetOption (table,BoolValue true)
+  	  VernacSetOption (use_locality_full(),table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
-  	  VernacUnsetOption table
+  	  VernacUnsetOption (use_locality_full(),table)
 
       | IDENT "Print"; IDENT "Table"; table = option_table ->
 	  VernacPrintOption table
@@ -779,10 +779,10 @@ GEXTEND Gram
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" -> 
-          VernacSetOption (["Ltac";"Debug"], BoolValue true)
+          VernacSetOption (None,["Ltac";"Debug"], BoolValue true)
 
       |	IDENT "Debug"; IDENT "Off" ->
-          VernacSetOption (["Ltac";"Debug"], BoolValue false)
+          VernacSetOption (None,["Ltac";"Debug"], BoolValue false)
 
  ] ];
     END
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 3bf2f0ede..656c38497 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -147,6 +147,10 @@ let pr_search a b pr_p = match a with
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b
 
+let pr_locality_full = function
+  | None -> mt()
+  | Some true -> str"Local "
+  | Some false -> str"Global "
 let pr_locality local = if local then str "Local " else str ""
 let pr_non_locality local = if local then str "" else str "Global "
 
@@ -854,9 +858,10 @@ let rec pr_vernac = function
                str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in
       hov 1 (pr_locality local ++ str"Strategy" ++ spc() ++
              hv 0 (prlist_with_sep sep pr_line l))
-  | VernacUnsetOption na ->
-      hov 1 (str"Unset" ++ spc() ++ pr_printoption na None)
-  | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v)
+  | VernacUnsetOption (l,na) ->
+      hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None)
+  | VernacSetOption (l,na,v) -> 
+      hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v)
   | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l))
   | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l))
   | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l))
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1de9d739a..0e11ba582 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -983,15 +983,15 @@ let vernac_set_opacity local str =
   let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in
   Redexpr.set_strategy local str
 
-let vernac_set_option key = function
-  | StringValue s -> set_string_option_value key s
-  | IntValue n -> set_int_option_value key (Some n)
-  | BoolValue b -> set_bool_option_value key b
+let vernac_set_option locality key = function
+  | StringValue s -> set_string_option_value_gen locality key s
+  | IntValue n -> set_int_option_value_gen locality key (Some n)
+  | BoolValue b -> set_bool_option_value_gen locality key b
 
-let vernac_unset_option key =
-  try set_bool_option_value key false
+let vernac_unset_option locality key =
+  try set_bool_option_value_gen locality key false
   with _ ->
-  set_int_option_value key None
+  set_int_option_value_gen locality key None
 
 let vernac_add_option key lv =
   let f = function
@@ -1371,8 +1371,8 @@ let interp c = match c with
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
-  | VernacSetOption (key,v) -> vernac_set_option key v
-  | VernacUnsetOption key -> vernac_unset_option key
+  | VernacSetOption (locality,key,v) -> vernac_set_option locality key v
+  | VernacUnsetOption (locality,key) -> vernac_unset_option locality 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
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ee86f982e..eaa434956 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -309,8 +309,8 @@ type vernac_expr =
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of
       locality_flag * (Conv_oracle.level * lreference list) list
-  | VernacUnsetOption of Goptions.option_name
-  | VernacSetOption of Goptions.option_name * option_value
+  | VernacUnsetOption of bool option * Goptions.option_name
+  | VernacSetOption of bool option * Goptions.option_name * option_value
   | 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
@@ -367,24 +367,21 @@ let check_locality () =
   if !locality_flag = Some false then
     syntax_checking_error "This command does not support the \"Global\" prefix."
 
-let use_locality () =
-  let local = match !locality_flag with Some true -> true | _ -> false in
+let use_locality_full () =
+  let r = !locality_flag in
   locality_flag := None;
-  local
+   r
+
+let use_locality () =
+  match use_locality_full () with Some true -> true | _ -> false 
 
 let use_locality_exp () = local_of_bool (use_locality ())
 
 let use_section_locality () =
-  let local = 
-    match !locality_flag with Some b -> b | None -> Lib.sections_are_opened ()
-  in
-  locality_flag := None;
-  local
+  match use_locality_full () with Some b -> b | None -> Lib.sections_are_opened ()
 
 let use_non_locality () =
-  let local = match !locality_flag with Some false -> false | _ -> true in
-  locality_flag := None;
-  local
+  match use_locality_full () with Some false -> false | _ -> true 
 
 let enforce_locality () =
   let local =