# HG changeset patch
# User clasohm
# Date 768830182 -7200
# Node ID 40d565e51deaa92a3bdc8882e82f4853c227f2b0
# Parent  3a853818f1d224c1ea4da956fef8c865826e6ee3
syntax_error now checks precedences when computing expected tokens

diff -r 3a853818f1d2 -r 40d565e51dea src/Pure/Syntax/parser.ML
--- 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 @