# HG changeset patch
# User wenzelm
# Date 1394119487 -3600
# Node ID cffb46aea3d1893a84673a1e7097aeeb030b39b5
# Parent  94d384d621b0673c871c6208757ed26b7eb62a87
more compact Markup.markup_report: message body may consist of multiple elements;

diff -r 94d384d621b0 -r cffb46aea3d1 src/Pure/General/name_space.ML
--- 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;
 
diff -r 94d384d621b0 -r cffb46aea3d1 src/Pure/Syntax/syntax_phases.ML
--- 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;