# 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 () =>