--- 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;
--- 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;
--- 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