more compact Markup.markup_report: message body may consist of multiple elements;
authorwenzelm
Thu, 06 Mar 2014 16:24:47 +0100
changeset 55957 cffb46aea3d1
parent 55956 94d384d621b0
child 55958 4ec984df4f45
more compact Markup.markup_report: message body may consist of multiple elements;
src/Pure/General/name_space.ML
src/Pure/Syntax/syntax_phases.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;
 
--- 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;