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, 13 insertions, 8 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ea686e5a3d..d10a2950ce 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 3bf2f0ede2..656c384973 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))