more compact Markup.markup_report: message body may consist of multiple elements;
--- a/src/Pure/General/name_space.ML Thu Mar 06 16:12:26 2014 +0100
+++ b/src/Pure/General/name_space.ML Thu Mar 06 16:24:47 2014 +0100
@@ -460,7 +460,7 @@
val completions = map (fn pos => completion context space (xname, pos)) ps;
in
error (undefined (kind_of space) name ^ Position.here_list ps ^
- implode (map (Markup.markup_report o Completion.reported_text) completions))
+ Markup.markup_report (implode (map Completion.reported_text completions)))
end)
end;
--- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 16:12:26 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 16:24:47 2014 +0100
@@ -323,7 +323,7 @@
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
- error (msg ^ implode (map (Markup.markup_report o Lexicon.reported_token_range ctxt) toks));
+ error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
val len = length pts;
val limit = Config.get ctxt Syntax.ambiguity_limit;