# HG changeset patch
# User clasohm
# Date 768474697 -7200
# Node ID b734dc03067ef412f6f5f3a104f04710b3660353
# Parent  5b6e4340085b6fa5b80360495d11d11626f65734
syntax_error now removes duplicate tokens in its output and doesn't
print the last unparsed token (i.e. EndToken)

diff -r 5b6e4340085b -r b734dc03067e src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri May 06 15:49:23 1994 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon May 09 11:11:37 1994 +0200
@@ -473,7 +473,8 @@
   ((if toks = [] then
       "error: unexpected end of input\n"
     else
-      "Syntax error at: " ^ quote (space_implode " " (map str_of_token toks))
+      "Syntax error at: " ^ quote (space_implode " " (map str_of_token 
+        ((rev o tl o rev) toks)))
       ^ "\n")
    ^ "Expected tokens: " 
    ^ space_implode ", " (map (quote o str_of_token) allowed));
@@ -495,10 +496,10 @@
               val NTs = map (fn (_, _, _, Nonterm (a, _) :: _, _, _) => a)
                             (filter (fn (_, _, _, Nonterm _ :: _, _, _) => true
                                      | _ => false) (Array.sub (stateset, i-1)));
-              val allowed = get_starts NTs union
+              val allowed = distinct (get_starts NTs @
                             (map (fn (_, _, _, Term a :: _, _, _) => a)
                             (filter (fn (_, _, _, Term _ :: _, _, _) => true
-                                    | _ => false) (Array.sub (stateset, i-1))));
+                                   | _ => false) (Array.sub (stateset, i-1)))));
                                              (*terminals have to be searched for
                                                because of lambda productions*)
           in syntax_error (if prev_token = EndToken then indata