# HG changeset patch # User wenzelm # Date 1289681184 -3600 # Node ID f51c478ef85ae9c7ce37e007f123db71d344178f # Parent 8ede48c93c7253d3e2618a251c0ee0cc085eaf7b always print state of proof commands (notably "qed" etc.); diff -r 8ede48c93c72 -r f51c478ef85a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Nov 13 21:01:03 2010 +0100 +++ b/src/Pure/PIDE/document.ML Sat Nov 13 21:46:24 2010 +0100 @@ -197,7 +197,7 @@ | NONE => ()); fun async_state tr st = - if Toplevel.print_of tr then + if Toplevel.print_of tr orelse Keyword.is_proof (Toplevel.name_of tr) then ignore (Future.fork_group (Task_Queue.new_group NONE) (fn () =>