# HG changeset patch
# User wenzelm
# Date 1218277692 -7200
# Node ID 851a1dfb7828e59728d7329e2f094cecca1540ce
# Parent  ece79c0597fe1f83fd643d40b62f524bd369fc0d
tuned error message;

diff -r ece79c0597fe -r 851a1dfb7828 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Aug 09 12:28:11 2008 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Aug 09 12:28:12 2008 +0200
@@ -788,12 +788,13 @@
     [] =>
       let
         val toks = if is_eof prev_token then indata else prev_token :: indata;
-        val pos = pos_of_token prev_token;
+        val pos = Position.str_of (pos_of_token prev_token);
       in
         if null toks then error ("Inner syntax error: unexpected end of input" ^ pos)
         else error (Pretty.string_of (Pretty.block
-          (Pretty.str ("Inner syntax error" ^ pos ^ " at: ") ::
-            Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))))))
+          (Pretty.str ("Inner syntax error" ^ pos ^ " at \"") ::
+            Pretty.breaks (map (Pretty.str o str_of_token) (#1 (split_last toks))) @
+            [Pretty.str "\""])))
       end
   | s =>
     (case indata of