# HG changeset patch
# User wenzelm
# Date 1392915076 -3600
# Node ID d5240907713575fbc29d6afe298e30ad69744b0a
# Parent  7aea773c55745c8a5efb93ccb9d3be738aa98ddc
tuned messages;

diff -r 7aea773c5574 -r d52409077135 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Feb 20 17:21:48 2014 +0100
+++ b/src/Pure/General/position.ML	Thu Feb 20 17:51:16 2014 +0100
@@ -187,15 +187,15 @@
 fun here pos =
   let
     val props = properties_of pos;
-    val s =
+    val (s1, s2) =
       (case (line_of pos, file_of pos) of
-        (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
-      | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
-      | (NONE, SOME name) => "(file " ^ quote name ^ ")"
-      | _ => if is_reported pos then "\\<here>" else "");
+        (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
+      | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
+      | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
+      | _ => if is_reported pos then ("", "\\<here>") else ("", ""));
   in
     if null props then ""
-    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
+    else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
 val here_list = space_implode " " o map here;
diff -r 7aea773c5574 -r d52409077135 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Feb 20 17:21:48 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Feb 20 17:51:16 2014 +0100
@@ -290,7 +290,9 @@
         (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
       (toks, []) => toks
     | (_, ss) =>
-        error (err_prefix ^ Symbol_Pos.content ss ^ Position.here (#1 (Symbol_Pos.range ss))))
+        error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^
+          Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss))))
+
   end;
 
 
diff -r 7aea773c5574 -r d52409077135 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Feb 20 17:21:48 2014 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Feb 20 17:51:16 2014 +0100
@@ -704,11 +704,18 @@
         val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
         val pos = Position.here (Lexicon.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 Lexicon.str_of_token) (#1 (split_last toks))) @
-            [Pretty.str "\""])))
+        if null toks then
+          error ("Inner syntax error: unexpected end of input" ^ pos)
+        else
+          error ("Inner syntax error" ^ pos ^
+            Markup.markup Markup.no_report
+              ("\n" ^ Pretty.string_of
+                (Pretty.block [
+                  Pretty.str "at", Pretty.brk 1,
+                  Pretty.block
+                   (Pretty.str "\"" ::
+                    Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
+                    [Pretty.str "\""])])))
       end
   | s =>
       (case indata of