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

2 files changed, 19 insertions, 22 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1de9d739a3..0e11ba582a 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 ee86f982e8..eaa434956f 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 =