From ea09770efde4a7bdd573407a408e54ec2b41b6ad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 8 Aug 2011 23:04:18 +0000
Subject: 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
---
 parsing/lexer.ml4 | 5 ++++-
 parsing/lexer.mli | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3