more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
authorwenzelm
Mon Jul 08 12:07:06 2013 +0200 (2013-07-08 ago)
changeset 52559ddaf277e0d8c
parent 52558 271663ddf289
child 52560 9e6b59cd5560
more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;
src/Pure/PIDE/command.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 08 12:00:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 08 12:07:06 2013 +0200
     1.3 @@ -252,10 +252,13 @@
     1.4  
     1.5  (* overall execution process *)
     1.6  
     1.7 +fun run_print ({name, pri, print_process, ...}: print) =
     1.8 +  (if Multithreading.enabled () then
     1.9 +    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
    1.10 +  else memo_eval) print_process;
    1.11 +
    1.12  fun execute (({eval_process, ...}, prints): exec) =
    1.13 - (memo_eval eval_process;
    1.14 -  prints |> List.app (fn {name, pri, print_process, ...} =>
    1.15 -    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
    1.16 +  (memo_eval eval_process; List.app run_print prints);
    1.17  
    1.18  fun stable_goals exec_id =
    1.19    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
     2.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:00:45 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Jul 08 12:07:06 2013 +0200
     2.3 @@ -188,13 +188,16 @@
     2.4      NONE => raise Runtime.TERMINATE
     2.5    | SOME line => map (read_chunk channel) (space_explode "," line));
     2.6  
     2.7 +fun worker_guest e =
     2.8 +  Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e ();
     2.9 +
    2.10  in
    2.11  
    2.12  fun loop channel =
    2.13    let val continue =
    2.14      (case read_command channel of
    2.15        [] => (Output.error_msg "Isabelle process: no input"; true)
    2.16 -    | name :: args => (run_command name args; true))
    2.17 +    | name :: args => (worker_guest (fn () => run_command name args); true))
    2.18      handle Runtime.TERMINATE => false
    2.19        | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
    2.20    in if continue then loop channel else () end;
    2.21 @@ -238,8 +241,6 @@
    2.22          Future.ML_statistics := true;
    2.23          Multithreading.trace := Options.int options "threads_trace";
    2.24          Multithreading.max_threads := Options.int options "threads";
    2.25 -        if Multithreading.max_threads_value () < 2
    2.26 -        then Multithreading.max_threads := 2 else ();
    2.27          Goal.skip_proofs := Options.bool options "editor_skip_proofs";
    2.28          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
    2.29        end);