diff -r 693a39f2cddc -r 3d5d949cd865 src/Pure/PIDE/execution.ML --- 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 _ =>