--- a/src/Pure/Thy/thy_syntax.ML Sat Nov 13 20:06:52 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sat Nov 13 20:13:35 2010 +0100
@@ -76,13 +76,17 @@
else I;
in props (token_kind_markup kind) end;
+fun report_symbol (sym, pos) =
+ if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
+
in
fun present_token tok =
Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
fun report_token tok =
- Position.report (Token.position_of tok) (token_markup tok);
+ (Position.report (Token.position_of tok) (token_markup tok);
+ List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
end;