--- a/src/Pure/Syntax/parser.ML Fri May 13 11:25:55 1994 +0200
+++ b/src/Pure/Syntax/parser.ML Fri May 13 13:56:22 1994 +0200
@@ -485,15 +485,20 @@
[] => let (*compute a list of allowed starting tokens
for a list of nonterminals*)
fun get_starts [] = []
- | get_starts (rhss_ref :: refs) =
+ | get_starts ((rhss_ref, minPrec:int) :: refs) =
let fun get [] = []
- | get ((Some tok, _) :: rhss) =
- tok :: (get rhss)
+ | get ((Some tok, prods) :: rhss) =
+ if exists (fn (Term _ :: _, _, prec) =>
+ prec >= minPrec
+ | (_, _, _) => false) prods
+ then tok :: (get rhss)
+ else get rhss
| get ((None, _) :: rhss) =
get rhss;
in (get (!rhss_ref)) union (get_starts refs) end;
- val NTs = map (fn (_, _, _, Nonterm (a, _) :: _, _, _) => a)
+ val NTs = map (fn (_, _, _, Nonterm (a, prec) :: _, _, _) =>
+ (a, prec))
(filter (fn (_, _, _, Nonterm _ :: _, _, _) => true
| _ => false) (Array.sub (stateset, i-1)));
val allowed = distinct (get_starts NTs @