1.1 --- a/src/Pure/System/isabelle_process.ML Mon Jul 08 12:00:45 2013 +0200
1.2 +++ b/src/Pure/System/isabelle_process.ML Mon Jul 08 12:07:06 2013 +0200
1.3 @@ -188,13 +188,16 @@
1.4 NONE => raise Runtime.TERMINATE
1.5 | SOME line => map (read_chunk channel) (space_explode "," line));
1.6
1.7 +fun worker_guest e =
1.8 + Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
1.9 +
1.10 in
1.11
1.12 fun loop channel =
1.13 let val continue =
1.14 (case read_command channel of
1.15 [] => (Output.error_msg "Isabelle process: no input"; true)
1.16 - | name :: args => (run_command name args; true))
1.17 + | name :: args => (worker_guest (fn () => run_command name args); true))
1.18 handle Runtime.TERMINATE => false
1.19 | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
1.20 in if continue then loop channel else () end;
1.21 @@ -238,8 +241,6 @@
1.22 Future.ML_statistics := true;
1.23 Multithreading.trace := Options.int options "threads_trace";
1.24 Multithreading.max_threads := Options.int options "threads";
1.25 - if Multithreading.max_threads_value () < 2
1.26 - then Multithreading.max_threads := 2 else ();
1.27 Goal.skip_proofs := Options.bool options "editor_skip_proofs";
1.28 Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
1.29 end);