src/Pure/PIDE/resources.ML
changeset 56294 85911b8a6868
parent 56286 7ede6ca96c61
child 56333 38f1422ef473
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Mar 26 14:15:34 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Mar 26 14:41:52 2014 +0100
     1.3 @@ -211,9 +211,10 @@
     1.4            val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
     1.5          in
     1.6            if strict then error msg
     1.7 -          else
     1.8 -            Context_Position.if_visible ctxt Output.report
     1.9 +          else if Context_Position.is_visible ctxt then
    1.10 +            Output.report
    1.11                (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
    1.12 +          else ()
    1.13          end;
    1.14    in path end;
    1.15