# HG changeset patch
# User wenzelm
# Date 1420800662 -3600
# Node ID b83d6c3c439a2c84eacde2c5c8b5c851836f7a01
# Parent  8a779359df67abc90c6120db085372e885796416
ignore print process even after fork, to avoid loosing active worker threads;

diff -r 8a779359df67 -r b83d6c3c439a src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Jan 09 10:49:35 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 09 11:51:02 2015 +0100
@@ -377,12 +377,15 @@
     else ()
   end;
 
+fun ignore_process process =
+  Lazy.is_running process orelse Lazy.is_finished process;
+
 fun run_eval execution_id (Eval {exec_id, eval_process}) =
   if Lazy.is_finished eval_process then ()
   else run_process execution_id exec_id eval_process;
 
 fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
-  if Lazy.is_running print_process orelse Lazy.is_finished print_process then ()
+  if ignore_process print_process then ()
   else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   then
     let
@@ -390,7 +393,9 @@
       fun fork () =
         ignore ((singleton o Future.forks)
           {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
-          (fn () => run_process execution_id exec_id print_process));
+          (fn () =>
+            if ignore_process print_process then ()
+            else run_process execution_id exec_id print_process));
     in
       (case delay of
         NONE => fork ()