src/Pure/Isar/toplevel.ML
changeset 38721 ca8b14fa0d0d
parent 38391 ba1cc1815ce1
child 38875 c7a66b584147
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 25 20:43:03 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 25 21:31:22 2010 +0200
     1.3 @@ -563,13 +563,6 @@
     1.4  fun status tr m =
     1.5    setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
     1.6  
     1.7 -fun async_state (tr as Transition {print, ...}) st =
     1.8 -  if print then
     1.9 -    ignore
    1.10 -      (Future.fork (fn () =>
    1.11 -          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
    1.12 -  else ();
    1.13 -
    1.14  fun error_msg tr exn_info =
    1.15    setmp_thread_position tr (fn () =>
    1.16      Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
    1.17 @@ -628,6 +621,22 @@
    1.18  
    1.19  (* managed execution *)
    1.20  
    1.21 +local
    1.22 +
    1.23 +fun async_state (tr as Transition {print, ...}) st =
    1.24 +  if print then
    1.25 +    ignore
    1.26 +      (Future.fork (fn () =>
    1.27 +          setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
    1.28 +  else ();
    1.29 +
    1.30 +fun proof_status tr st =
    1.31 +  (case try proof_of st of
    1.32 +    SOME prf => status tr (Proof.status_markup prf)
    1.33 +  | NONE => ());
    1.34 +
    1.35 +in
    1.36 +
    1.37  fun run_command thy_name tr st =
    1.38    (case
    1.39        (case init_of tr of
    1.40 @@ -637,13 +646,18 @@
    1.41        let val int = is_some (init_of tr) in
    1.42          (case transition int tr st of
    1.43            SOME (st', NONE) =>
    1.44 -            (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
    1.45 +           (status tr Markup.finished;
    1.46 +            proof_status tr st';
    1.47 +            if int then () else async_state tr st';
    1.48 +            SOME st')
    1.49          | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.50          | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.51          | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.52        end
    1.53    | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    1.54  
    1.55 +end;
    1.56 +
    1.57  
    1.58  (* nested commands *)
    1.59