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