more compact Markup.markup_report: message body may consist of multiple elements;
authorwenzelm
Thu Mar 06 16:24:47 2014 +0100 (2014-03-06)
changeset 55957cffb46aea3d1
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
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 06 16:12:26 2014 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 06 16:24:47 2014 +0100
     1.3 @@ -460,7 +460,7 @@
     1.4            val completions = map (fn pos => completion context space (xname, pos)) ps;
     1.5          in
     1.6            error (undefined (kind_of space) name ^ Position.here_list ps ^
     1.7 -            implode (map (Markup.markup_report o Completion.reported_text) completions))
     1.8 +            Markup.markup_report (implode (map Completion.reported_text completions)))
     1.9          end)
    1.10    end;
    1.11  
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:12:26 2014 +0100
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 16:24:47 2014 +0100
     2.3 @@ -323,7 +323,7 @@
     2.4  
     2.5      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
     2.6        handle ERROR msg =>
     2.7 -        error (msg ^ implode (map (Markup.markup_report o Lexicon.reported_token_range ctxt) toks));
     2.8 +        error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
     2.9      val len = length pts;
    2.10  
    2.11      val limit = Config.get ctxt Syntax.ambiguity_limit;