more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;

--- a/src/Pure/PIDE/command.ML	Mon Jul 08 12:00:45 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 08 12:07:06 2013 +0200
@@ -252,10 +252,13 @@
 
 (* overall execution process *)
 
+fun run_print ({name, pri, print_process, ...}: print) =
+  (if Multithreading.enabled () then
+    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
+  else memo_eval) print_process;
+
 fun execute (({eval_process, ...}, prints): exec) =
- (memo_eval eval_process;
-  prints |> List.app (fn {name, pri, print_process, ...} =>
-    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
+  (memo_eval eval_process; List.app run_print prints);
 
 fun stable_goals exec_id =
   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));

--- a/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:00:45 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:07:06 2013 +0200
@@ -188,13 +188,16 @@
     NONE => raise Runtime.TERMINATE
   | SOME line => map (read_chunk channel) (space_explode "," line));
 
+fun worker_guest e =
+  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
+
 in
 
 fun loop channel =
   let val continue =
     (case read_command channel of
       [] => (Output.error_msg "Isabelle process: no input"; true)
-    | name :: args => (run_command name args; true))
+    | name :: args => (worker_guest (fn () => run_command name args); true))
     handle Runtime.TERMINATE => false
       | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
   in if continue then loop channel else () end;
@@ -238,8 +241,6 @@
         Future.ML_statistics := true;
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
-        if Multithreading.max_threads_value () < 2
-        then Multithreading.max_threads := 2 else ();
         Goal.skip_proofs := Options.bool options "editor_skip_proofs";
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
       end);