no print_state for final proof commands, which return to theory state;
authorwenzelm
Wed Sep 07 21:31:50 2011 +0200 (2011-09-07)
changeset 448043d9ee91394ce
parent 44803 aecfefb05731
child 44805 48a5c104d434
no print_state for final proof commands, which return to theory state;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Sep 07 21:10:47 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Sep 07 21:31:50 2011 +0200
     1.3 @@ -331,7 +331,6 @@
     1.4    let
     1.5      val is_init = Toplevel.is_init tr;
     1.6      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
     1.7 -    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
     1.8  
     1.9      val _ = Multithreading.interrupted ();
    1.10      val _ = Toplevel.status tr Markup.forked;
    1.11 @@ -343,13 +342,18 @@
    1.12    in
    1.13      (case result of
    1.14        NONE =>
    1.15 -       (if null errs then Exn.interrupt () else ();
    1.16 -        Toplevel.status tr Markup.failed;
    1.17 -        (st, no_print))
    1.18 +        let
    1.19 +          val _ = if null errs then Exn.interrupt () else ();
    1.20 +          val _ = Toplevel.status tr Markup.failed;
    1.21 +        in (st, no_print) end
    1.22      | SOME st' =>
    1.23 -       (Toplevel.status tr Markup.finished;
    1.24 -        proof_status tr st';
    1.25 -        (st', if do_print then print_state tr st' else no_print)))
    1.26 +        let
    1.27 +          val _ = Toplevel.status tr Markup.finished;
    1.28 +          val _ = proof_status tr st';
    1.29 +          val do_print =
    1.30 +            not is_init andalso
    1.31 +              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.32 +        in (st', if do_print then print_state tr st' else no_print) end)
    1.33    end;
    1.34  
    1.35  end;