--- a/src/Pure/Syntax/syntax.ML Fri Sep 17 20:56:32 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Sep 17 21:04:56 2010 +0200
@@ -710,7 +710,9 @@
val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
- handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
+ handle ERROR msg =>
+ error (msg ^
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;