src/Pure/PIDE/document.ML
changeset 40534 9e196062bf88
parent 40532 f51c478ef85a
child 41537 3837045cc8a1
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Nov 13 22:33:07 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Nov 14 14:05:08 2010 +0100
     1.3 @@ -197,13 +197,11 @@
     1.4    | NONE => ());
     1.5  
     1.6  fun async_state tr st =
     1.7 -  if Toplevel.print_of tr orelse Keyword.is_proof (Toplevel.name_of tr) then
     1.8 -    ignore
     1.9 -      (Future.fork_group (Task_Queue.new_group NONE)
    1.10 -        (fn () =>
    1.11 -          Toplevel.setmp_thread_position tr
    1.12 -            (fn () => Toplevel.print_state false st) ()))
    1.13 -  else ();
    1.14 +  ignore
    1.15 +    (Future.fork_group (Task_Queue.new_group NONE)
    1.16 +      (fn () =>
    1.17 +        Toplevel.setmp_thread_position tr
    1.18 +          (fn () => Toplevel.print_state false st) ()));
    1.19  
    1.20  fun run int tr st =
    1.21    (case Toplevel.transition int tr st of
    1.22 @@ -223,9 +221,12 @@
    1.23        | NONE => Exn.Result ()) of
    1.24      Exn.Result () =>
    1.25        let
    1.26 -        val int = is_some (Toplevel.init_of tr);
    1.27 +        val is_init = is_some (Toplevel.init_of tr);
    1.28 +        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.29 +        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
    1.30 +
    1.31          val start = start_timing ();
    1.32 -        val (errs, result) = run int tr st;
    1.33 +        val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.34          val _ = timing tr (end_timing start);
    1.35          val _ = List.app (Toplevel.error_msg tr) errs;
    1.36          val res =
    1.37 @@ -234,7 +235,7 @@
    1.38            | SOME st' =>
    1.39               (Toplevel.status tr Markup.finished;
    1.40                proof_status tr st';
    1.41 -              if int then () else async_state tr st';
    1.42 +              if do_print then async_state tr st' else ();
    1.43                (true, st')));
    1.44        in res end
    1.45    | Exn.Exn exn =>