--- a/src/Pure/PIDE/document.ML Sat Nov 13 22:33:07 2010 +0100
+++ b/src/Pure/PIDE/document.ML Sun Nov 14 14:05:08 2010 +0100
@@ -197,13 +197,11 @@
| NONE => ());
fun async_state tr st =
- if Toplevel.print_of tr orelse Keyword.is_proof (Toplevel.name_of tr) then
- ignore
- (Future.fork_group (Task_Queue.new_group NONE)
- (fn () =>
- Toplevel.setmp_thread_position tr
- (fn () => Toplevel.print_state false st) ()))
- else ();
+ ignore
+ (Future.fork_group (Task_Queue.new_group NONE)
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Toplevel.print_state false st) ()));
fun run int tr st =
(case Toplevel.transition int tr st of
@@ -223,9 +221,12 @@
| NONE => Exn.Result ()) of
Exn.Result () =>
let
- val int = is_some (Toplevel.init_of tr);
+ val is_init = is_some (Toplevel.init_of tr);
+ val is_proof = Keyword.is_proof (Toplevel.name_of tr);
+ val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
+
val start = start_timing ();
- val (errs, result) = run int tr st;
+ val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
val _ = timing tr (end_timing start);
val _ = List.app (Toplevel.error_msg tr) errs;
val res =
@@ -234,7 +235,7 @@
| SOME st' =>
(Toplevel.status tr Markup.finished;
proof_status tr st';
- if int then () else async_state tr st';
+ if do_print then async_state tr st' else ();
(true, st')));
in res end
| Exn.Exn exn =>