avoid duplicate printing of 'theory' state (cf. 173974e07dea);
authorwenzelm
Tue Jul 20 21:07:23 2010 +0200 (2010-07-20 ago)
changeset 37859575a14dd4167
parent 37858 e1ef6b441fe7
child 37860 aa3b3d00698b
avoid duplicate printing of 'theory' state (cf. 173974e07dea);
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 20 20:56:28 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 20 21:07:23 2010 +0200
     1.3 @@ -633,11 +633,14 @@
     1.4          SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
     1.5        | NONE => Exn.Result ()) of
     1.6      Exn.Result () =>
     1.7 -      (case transition (is_some (init_of tr)) tr st of
     1.8 -        SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
     1.9 -      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.10 -      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.11 -      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.12 +      let val int = is_some (init_of tr) in
    1.13 +        (case transition int tr st of
    1.14 +          SOME (st', NONE) =>
    1.15 +            (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
    1.16 +        | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.17 +        | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.18 +        | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.19 +      end
    1.20    | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    1.21  
    1.22