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

1 files changed, 18 insertions, 26 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 79b3dac5f7..551ff302ae 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -308,16 +308,12 @@ let rec interp_list_parser hd = function
       xyl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
-
 (* Find non-terminal tokens of notation *)
 
-let is_normal_token str =
-  try let _ = Lexer.check_ident str in true with Lexer.Error.E _ -> false
-
 (* To protect alphabetic tokens and quotes from being seen as variables *)
 let quote_notation_token x =
   let n = String.length x in
-  let norm = is_normal_token x in
+  let norm = is_ident x in
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
@@ -325,7 +321,7 @@ let rec raw_analyze_notation_tokens = function
   | []    -> []
   | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
   | String "_" :: _ -> error "_ must be quoted."
-  | String x :: sl when is_normal_token x ->
+  | String x :: sl when is_ident x ->
       NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -579,27 +575,23 @@ let hunks_of_format (from,(vars,typs)) symfmt =
 
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
-let is_not_small_constr = function
-    ETConstr _ -> true
-  | ETOther("constr","binder_constr") -> true
-  | _ -> false
-
-let rec define_keywords_aux = function
-  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
-      when is_not_small_constr e ->
-      message ("Defining '"^k^"' as keyword");
-      Lexer.add_keyword k;
-      n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
-  | n :: l -> n :: define_keywords_aux l
-  | [] -> []
+let constr_level n = function
+  | ETConstr (NextLevel,_) -> n-1
+  | ETConstr (NumLevel n,_) -> n
+  | ETOther("constr","binder_constr") -> 200
+  | _ -> 0
 
   (* Ensure that IDENT articulation terminal symbols are keywords *)
-let define_keywords = function
-  | GramConstrTerminal(IDENT k)::l ->
+let rec define_keywords n = function
+  | GramConstrNonTerminal(e,Some _) as x1 :: GramConstrTerminal(IDENT k) :: l
+      when constr_level n e > 9 ->
+      (* an entry can catch an ident coming next if it is at a level *)
+      (* higher than the level of applications which is 10 *)
       message ("Defining '"^k^"' as keyword");
       Lexer.add_keyword k;
-      GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
-  | l -> define_keywords_aux l
+      x1 :: GramConstrTerminal(KEYWORD k) :: define_keywords n l
+  | x :: l -> x :: define_keywords  n l
+  | [] -> []
 
 let distribute a ll = List.map (fun l -> a @ l) ll
 
@@ -618,7 +610,7 @@ let rec expand_list_rule typ tkl x n i hds ll =
     distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @
       expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll
 
-let make_production etyps symbols =
+let make_production n etyps symbols =
   let prod =
     List.fold_right
       (fun t ll -> match t with
@@ -642,7 +634,7 @@ let make_production etyps symbols =
             | _ ->
                 error "Components of recursive patterns in notation must be terms or binders.")
       symbols [[]] in
-  List.map define_keywords prod
+  List.map (define_keywords n) prod
 
 let rec find_symbols c_current c_next c_last = function
   | [] -> []
@@ -1013,7 +1005,7 @@ let recover_notation_syntax rawntn =
 
 let make_pa_rule (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
-  let prod = make_production typs symbols in
+  let prod = make_production n typs symbols in
   (n,assoc,ntn,prod)
 
 let make_pp_rule (n,typs,symbols,fmt) =