# HG changeset patch
# User wenzelm
# Date 1203021224 -3600
# Node ID 321c4ca82923176c1fbf1043d2446b3a22f839df
# Parent  3d2a4fd4ed7759051b1ae517910eda55e3a5f555
syntax error: suppress expected categories altogether;

diff -r 3d2a4fd4ed77 -r 321c4ca82923 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Feb 14 15:45:26 2008 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Feb 14 21:33:44 2008 +0100
@@ -53,9 +53,6 @@
                          lambda productions are stored as normal productions
                          and also as an entry in "lambdas"*)
 
-fun reverted_tags (tags: nt_tag Symtab.table) =
-  the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
-
 val UnknownStart = EndToken;       (*productions for which no starting token is
                                      known yet are associated with this token*)
 
@@ -395,7 +392,7 @@
   let
     fun pretty_name name = [Pretty.str (name ^ " =")];
 
-    val nt_name = reverted_tags tags;
+    val nt_name = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
     fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s)
       | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
@@ -793,23 +790,13 @@
           if prev_token = EndToken then indata
           else prev_token :: indata;
 
-        val nt_name = reverted_tags tags;
-        val nts =
-          fold (fn (_, _, _, Nonterminal (tag, p) :: _, _, _) =>
-            AList.map_default (op =) (tag, p) (fn p' => Int.min (p, p')) | _ => I)
-            (Array.sub (stateset, i - 1)) []
-          |> map (fn (a, prec) => nt_name a ^ "[" ^ signed_string_of_int prec ^ "]");
-
         val msg =
-          (if null toks then Pretty.str "Inner syntax error: unexpected end of input"
-           else
-             Pretty.block (Pretty.str "Inner syntax error at: \"" ::
-               Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))) @
-               [Pretty.str "\""])) ::
-          (if null nts then []
-           else [Pretty.block
-            (Pretty.str "Expected syntax categories: " :: Pretty.commas (map Pretty.str nts))]);
-      in error (Pretty.string_of (Pretty.chunks msg)) end
+          if null toks then Pretty.str "Inner syntax error: unexpected end of input"
+          else
+            Pretty.block (Pretty.str "Inner syntax error at: \"" ::
+              Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))) @
+              [Pretty.str "\""]);
+      in error (Pretty.string_of msg) end
   | s =>
     (case indata of
        [] => Array.sub (stateset, i)