Ajout possibilité d'options à trois mots.

Suppression au passage syntaxe "Set table field ref", synonyme de "Add
table field ref" et de "Unset table field ref", synonyme de "Remove
table field ref".  Changement de la syntaxe "Test tabel field val" en
""Test tabel field for val".


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

2 files changed, 31 insertions, 30 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6d0e3ffc43..ce9aacee81 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -551,48 +551,41 @@ GEXTEND Gram
 	  VernacAddMLPath (true, dir)
 
       (* Pour intervenir sur les tables de param��tres *)
-      | "Set"; table = IDENT; field = IDENT; v = option_value ->
-  	  VernacSetOption (SecondaryTable (table,field),v)
-      | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
-  	  VernacAddOption (SecondaryTable (table,field),lv)
-      | "Set"; table = IDENT; field = IDENT ->
-  	  VernacSetOption (SecondaryTable (table,field),BoolValue true)
-      | IDENT "Unset"; table = IDENT; field = IDENT ->
-  	  VernacUnsetOption (SecondaryTable (table,field))
-      | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
-  	  VernacRemoveOption (SecondaryTable (table,field),lv)
-      | "Set"; table = IDENT; value = option_value ->
-  	  VernacSetOption (PrimaryTable table, value)
-      | "Set"; table = IDENT ->
-  	  VernacSetOption (PrimaryTable table, BoolValue true)
-      | IDENT "Unset"; table = IDENT ->
-  	  VernacUnsetOption (PrimaryTable table)
-
-      | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT ->
-	  VernacPrintOption (SecondaryTable (table,field))
-      | IDENT "Print"; IDENT "Table"; table = IDENT ->
-	  VernacPrintOption (PrimaryTable table)
+      | "Set"; table = option_table; v = option_value ->
+  	  VernacSetOption (table,v)
+      | "Set"; table = option_table ->
+  	  VernacSetOption (table,BoolValue true)
+      | IDENT "Unset"; table = option_table ->
+  	  VernacUnsetOption table
+
+      | IDENT "Print"; IDENT "Table"; table = option_table ->
+	  VernacPrintOption table
 
       | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
         -> VernacAddOption (SecondaryTable (table,field), v)
-
       (* Un value global ci-dessous va ��tre cach�� par un field au dessus! *)
+      (* Dans la pratique, on a donn�� priorit�� aux tables secondaires *)
       | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
           VernacAddOption (PrimaryTable table, v)
+      | IDENT "Add"; table = IDENT; field = IDENT; field2 = IDENT; 
+	  v = LIST1 option_ref_value
+        -> VernacAddOption (TertiaryTable (table,field,field2), v)
 
-      | IDENT "Test"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
-        -> VernacMemOption (SecondaryTable (table,field), v)
-      | IDENT "Test"; table = IDENT; field = IDENT ->
-          VernacPrintOption (SecondaryTable (table,field))
-      | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value ->
-          VernacMemOption (PrimaryTable table, v)
-      | IDENT "Test"; table = IDENT ->
-          VernacPrintOption (PrimaryTable table)
+      | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
+        -> VernacMemOption (table, v)
+      | IDENT "Test"; table = option_table ->
+          VernacPrintOption table
 
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
         -> VernacRemoveOption (SecondaryTable (table,field), v)
+      (* Un value global ci-dessous va ��tre cach�� par un field au dessus! *)
+      (* Dans la pratique, on a donn�� priorit�� aux tables secondaires *)
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
 	  VernacRemoveOption (PrimaryTable table, v) 
+      | IDENT "Remove"; table = IDENT; field = IDENT; field2 = IDENT; 
+	  v = LIST1 option_ref_value ->
+	  VernacRemoveOption (TertiaryTable (table,field,field2), v) 
+
       | IDENT "proof" -> VernacDeclProof
       | "return" -> VernacReturn ]]
   ;
@@ -657,6 +650,11 @@ GEXTEND Gram
     [ [ id = global   -> QualidRefValue id
       | s  = STRING   -> StringRefValue s ] ]
   ;
+  option_table:
+    [ [ f1 = IDENT; f2 = IDENT; f3 = IDENT -> TertiaryTable (f1,f2,f3)
+      | f1 = IDENT; f2 = IDENT -> SecondaryTable (f1,f2)
+      | f1 = IDENT -> PrimaryTable f1 ] ]
+  ;
   as_dirpath:
     [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
   ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9b01863680..e9d960e37c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -162,6 +162,9 @@ let pr_option_ref_value = function
 let pr_printoption a b = match a with
   | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
   | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b
+  | Goptions.TertiaryTable (table,field1,field2) -> str table ++ spc() ++
+      str field1 ++ spc() ++ str field2 ++ 
+      pr_opt (prlist_with_sep sep pr_option_ref_value) b
 
 let pr_set_option a b = 
   let pr_opt_value = function