diff -r 9c4809ec28ef -r 0f9a4e8ee1ab src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Sep 06 16:11:19 2019 +0200 +++ b/src/Pure/PIDE/command.ML Fri Sep 06 16:48:28 2019 +0200 @@ -233,7 +233,7 @@ Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); fun status tr m = - Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); + Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) (); fun command_indent tr st = (case try Toplevel.proof_of st of