# HG changeset patch # User wenzelm # Date 1289675615 -3600 # Node ID d5e9f760834190e49225c1198c546a09c66866a9 # Parent e0c000e40c056fe09ca2a29eaf161018ab712a61 report malformed symbols; diff -r e0c000e40c05 -r d5e9f7608341 src/Pure/Thy/thy_syntax.ML --- 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;