1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jul 03 20:36:30 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jul 03 22:33:10 2010 +0200
     1.3 @@ -86,9 +86,9 @@
     1.4    val error_msg: transition -> exn * string -> unit
     1.5    val add_hook: (transition -> state -> state -> unit) -> unit
     1.6    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.7 +  val run_command: string -> transition -> state -> state option
     1.8    val commit_exit: Position.T -> transition
     1.9    val command: transition -> state -> state
    1.10 -  val run_command: string -> transition -> state -> state option
    1.11    val excursion: (transition * transition list) list -> (transition * state) list lazy
    1.12  end;
    1.13  
    1.14 @@ -561,6 +561,10 @@
    1.15  fun status tr m =
    1.16    setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
    1.17  
    1.18 +fun async_state tr st =
    1.19 +  Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
    1.20 +    setmp_thread_position tr (fn () => print_state false st) ());
    1.21 +
    1.22  fun error_msg tr exn_info =
    1.23    setmp_thread_position tr (fn () =>
    1.24      Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
    1.25 @@ -614,6 +618,22 @@
    1.26  end;
    1.27  
    1.28  
    1.29 +(* managed execution *)
    1.30 +
    1.31 +fun run_command thy_name (tr as Transition {print, ...}) st =
    1.32 +  (case
    1.33 +      (case init_of tr of
    1.34 +        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
    1.35 +      | NONE => Exn.Result ()) of
    1.36 +    Exn.Result () =>
    1.37 +      (case transition false tr st of
    1.38 +        SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
    1.39 +      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.40 +      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.41 +      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.42 +  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    1.43 +
    1.44 +
    1.45  (* commit final exit *)
    1.46  
    1.47  fun commit_exit pos =
    1.48 @@ -635,19 +655,6 @@
    1.49    let val st' = command tr st
    1.50    in (st', st') end;
    1.51  
    1.52 -fun run_command thy_name tr st =
    1.53 -  (case
    1.54 -      (case init_of tr of
    1.55 -        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
    1.56 -      | NONE => Exn.Result ()) of
    1.57 -    Exn.Result () =>
    1.58 -      (case transition true tr st of
    1.59 -        SOME (st', NONE) => (status tr Markup.finished; SOME st')
    1.60 -      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
    1.61 -      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.62 -      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.63 -  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    1.64 -
    1.65  
    1.66  (* excursion of units, consisting of commands with proof *)
    1.67  

     2.1 --- a/src/Pure/System/isabelle_process.ML	Sat Jul 03 20:36:30 2010 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Sat Jul 03 22:33:10 2010 +0200
     2.3 @@ -91,6 +91,7 @@
     2.4   (Unsynchronized.change print_mode
     2.5      (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
     2.6    setup_channels out |> init_message;
     2.7 +  quick_and_dirty := true;  (* FIXME !? *)
     2.8    Keyword.report ();
     2.9    Output.status (Markup.markup Markup.ready "");
    2.10    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});