| 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;