KEYID token makes parsing more robust in face of notations

A notation may introduce a new keyword that masks an quasi keyword
(IDENT "of" for example) used in some grammar rules.  KEYID "of"
acepts both "of" as an ident and "of" as a keyword.  Rephrasing grammar
rules with KEYID makes hence them more robust in face of user notations.

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

1 files changed, 13 insertions, 1 deletions

diff --git a/parsing/tok.ml b/parsing/tok.ml
index 4cb94e38b..6c256c0c7 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -13,6 +13,7 @@ type t =
   | METAIDENT of string
   | PATTERNIDENT of string
   | IDENT of string
+  | KEYID of string
   | FIELD of string
   | INT of string
   | STRING of string
@@ -22,6 +23,7 @@ type t =
 let extract_string = function
   | KEYWORD s -> s
   | IDENT s -> s
+  | KEYID s -> s
   | STRING s -> s
   | METAIDENT s -> s
   | PATTERNIDENT s -> s
@@ -33,6 +35,7 @@ let extract_string = function
 let to_string = function
   | KEYWORD s -> Format.sprintf "%S" s
   | IDENT s -> Format.sprintf "IDENT %S" s
+  | KEYID s -> Format.sprintf "KEYID %S" s
   | METAIDENT s -> Format.sprintf "METAIDENT %S" s
   | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
   | FIELD s -> Format.sprintf "FIELD %S" s
@@ -43,6 +46,7 @@ let to_string = function
 
 let match_keyword kwd = function
   | KEYWORD kwd' when kwd = kwd' -> true
+  | KEYID kwd' when kwd = kwd' -> true
   | _ -> false
 
 (* Needed to fix Camlp4 signature.
@@ -55,6 +59,7 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok)
 let of_pattern = function
   | "", s -> KEYWORD s
   | "IDENT", s -> IDENT s
+  | "KEYID", s -> KEYID s
   | "METAIDENT", s -> METAIDENT s
   | "PATTERNIDENT", s -> PATTERNIDENT s
   | "FIELD", s -> FIELD s
@@ -67,6 +72,7 @@ let of_pattern = function
 let to_pattern = function
   | KEYWORD s -> "", s
   | IDENT s -> "IDENT", s
+  | KEYID s -> "KEYID", s
   | METAIDENT s -> "METAIDENT", s
   | PATTERNIDENT s -> "PATTERNIDENT", s
   | FIELD s -> "FIELD", s
@@ -80,6 +86,7 @@ let match_pattern =
   function
     | "", "" -> (function KEYWORD s -> s | _ -> err ())
     | "IDENT", "" -> (function IDENT s -> s | _ -> err ())
+    | "KEYID", "" -> (function _ -> err ())
     | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ())
     | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
     | "FIELD", "" -> (function FIELD s -> s | _ -> err ())
@@ -89,4 +96,9 @@ let match_pattern =
     | "EOI", "" -> (function EOI -> "" | _ -> err ())
     | pat ->
 	let tok = of_pattern pat in
-	function tok' -> if tok = tok' then snd pat else err ()
+	function tok' -> 
+          match tok, tok' with
+          | KEYID s, KEYWORD s' when s = s' -> snd pat
+          | KEYID s, IDENT s' when s = s' -> snd pat
+          | _, KEYID _ -> assert false
+          | _ -> if tok = tok' then snd pat else err ()