src/Pure/PIDE/resources.ML
changeset 56333 38f1422ef473
parent 56294 85911b8a6868
child 56803 d3cc56ca54c9
     1.1 --- a/src/Pure/PIDE/resources.ML	Sun Mar 30 21:24:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Mar 31 10:28:08 2014 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4            if strict then error msg
     1.5            else if Context_Position.is_visible ctxt then
     1.6              Output.report
     1.7 -              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
     1.8 +              [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
     1.9            else ()
    1.10          end;
    1.11    in path end;