# HG changeset patch
# User wenzelm
# Date 1279652843 -7200
# Node ID 575a14dd41673555895345cbcb6b808856412156
# Parent  e1ef6b441fe79e9d1e2e960c9a8d8bbdc88a3993
avoid duplicate printing of 'theory' state (cf. 173974e07dea);

diff -r e1ef6b441fe7 -r 575a14dd4167 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 20:56:28 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 21:07:23 2010 +0200
@@ -633,11 +633,14 @@
         SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
-      (case transition (is_some (init_of tr)) tr st of
-        SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
-      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
-      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
-      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
+      let val int = is_some (init_of tr) in
+        (case transition int tr st of
+          SOME (st', NONE) =>
+            (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
+        | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
+        | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
+        | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
+      end
   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));