# HG changeset patch
# User wenzelm
# Date 889456257 -3600
# Node ID 44e33cfdbb46f17abb13c6b6199d0b1f4b1ff967
# Parent  101d384b69b2fb9a82a68983dca03e45a078c170
tuned syntax error msg;

diff -r 101d384b69b2 -r 44e33cfdbb46 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Mar 09 16:10:38 1998 +0100
+++ b/src/Pure/Syntax/parser.ML	Mon Mar 09 16:10:57 1998 +0100
@@ -787,15 +787,18 @@
 
 
 fun syntax_error toks allowed =
-  error 
-  ((if toks = [] then
-      "error: unexpected end of input\n"
-    else
-      "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));
+  let
+    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) (rev (tl (rev toks)))) @
+          [Pretty.str "\""]);
+    val expected =
+      Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed);
+  in
+    error (Pretty.string_of (Pretty.blk (0, [msg, Pretty.fbrk, expected])))
+  end;
 
 fun produce prods chains stateset i indata prev_token =
                                       (*prev_token is used for error messages*)