Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);

--- a/src/Pure/Isar/toplevel.ML	Sat Jul 03 20:36:30 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jul 03 22:33:10 2010 +0200
@@ -86,9 +86,9 @@
   val error_msg: transition -> exn * string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
+  val run_command: string -> transition -> state -> state option
   val commit_exit: Position.T -> transition
   val command: transition -> state -> state
-  val run_command: string -> transition -> state -> state option
   val excursion: (transition * transition list) list -> (transition * state) list lazy
 end;
 
@@ -561,6 +561,10 @@
 fun status tr m =
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
+fun async_state tr st =
+  Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
+    setmp_thread_position tr (fn () => print_state false st) ());
+
 fun error_msg tr exn_info =
   setmp_thread_position tr (fn () =>
     Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
@@ -614,6 +618,22 @@
 end;
 
 
+(* managed execution *)
+
+fun run_command thy_name (tr as Transition {print, ...}) st =
+  (case
+      (case init_of tr of
+        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
+      | NONE => Exn.Result ()) of
+    Exn.Result () =>
+      (case transition false 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))
+  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
+
+
 (* commit final exit *)
 
 fun commit_exit pos =
@@ -635,19 +655,6 @@
   let val st' = command tr st
   in (st', st') end;
 
-fun run_command thy_name tr st =
-  (case
-      (case init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
-      | NONE => Exn.Result ()) of
-    Exn.Result () =>
-      (case transition true tr st of
-        SOME (st', NONE) => (status tr Markup.finished; 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))
-  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
-
 
 (* excursion of units, consisting of commands with proof *)
 

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