Be a bit less aggressive in declaring idents as keywords in notations

(an articulating ident needs to be a keyword if the constr entry that
 preceeds it is higher than the level of applications).

Also fixed is_ident_not_keyword which only looked at the first letter
and at the keyword status to decide if a token is an ident. This
allowed to simplified define_keywords in Metasyntax.

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

2 files changed, 5 insertions, 1 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c94b42c28c..581d151d1c 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -205,6 +205,9 @@ let check_ident str =
   in
   loop_id false (Stream.of_string str)
 
+let is_ident str =
+  try let _ = check_ident str in true with Error.E _ -> false
+
 (* Keyword and symbol dictionary *)
 let token_tree = ref empty_ttree
 
@@ -609,7 +612,7 @@ END
 
 let is_ident_not_keyword s =
   match s.[0] with
-    | 'a'..'z' | 'A'..'Z' | '_' -> not (is_keyword s)
+    | 'a'..'z' | 'A'..'Z' | '_' -> is_ident s && not (is_keyword s)
     | _ -> false
 
 let is_number s =
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 0a40d07276..1899f7f4d5 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -21,6 +21,7 @@ val location_table : unit -> location_table
 val restore_location_table : location_table -> unit
 
 val check_ident : string -> unit
+val is_ident : string -> bool
 val check_keyword : string -> unit
 
 type frozen_t