src/Pure/PIDE/execution.ML
changeset 73101 3d5d949cd865
parent 70662 0f9a4e8ee1ab
child 78757 a094bf81a496
--- a/src/Pure/PIDE/execution.ML	Fri Jan 08 15:03:51 2021 +0100
+++ b/src/Pure/PIDE/execution.ML	Fri Jan 08 15:07:25 2021 +0100
@@ -174,7 +174,7 @@
                     Exn.Exn exn =>
                      (status task [Markup.failed];
                       status task [Markup.finished];
-                      Output.report [Markup.markup_only (Markup.bad ())];
+                      Position.report pos (Markup.bad ());
                       if exec_id = 0 then ()
                       else List.app (Future.error_message pos) (Runtime.exn_messages exn))
                   | Exn.Res _ =>