future_job: explicit indication of interrupts;

--- a/src/Pure/Concurrent/future.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -41,9 +41,10 @@
   val is_finished: 'a future -> bool
   val cancel_group: Task_Queue.group -> unit
   val cancel: 'a future -> unit
-  val forks:
-    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
-      (unit -> 'a) list -> 'a future list
+  type fork_params =
+   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
+    pri: int, interrupts: bool}
+  val forks: fork_params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
@@ -51,9 +52,7 @@
   val join: 'a future -> 'a
   val value: 'a -> 'a future
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val cond_forks:
-    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
-      (unit -> 'a) list -> 'a future list
+  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val promise_group: Task_Queue.group -> 'a future
   val promise: unit -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -403,7 +402,7 @@
       | Exn.Res _ => true);
   in ok end;
 
-fun future_job group (e: unit -> 'a) =
+fun future_job group interrupts (e: unit -> 'a) =
   let
     val result = Single_Assignment.var "future" : 'a result;
     val pos = Position.thread_data ();
@@ -412,7 +411,9 @@
         val res =
           if ok then
             Exn.capture (fn () =>
-              Multithreading.with_attributes Multithreading.private_interrupts
+              Multithreading.with_attributes
+                (if interrupts
+                 then Multithreading.private_interrupts else Multithreading.no_interrupts)
                 (fn _ => Position.setmp_thread_data pos e ()) before
               Multithreading.interrupted ()) ()
           else Exn.interrupt_exn;
@@ -422,7 +423,11 @@
 
 (* fork *)
 
-fun forks {name, group, deps, pri} es =
+type fork_params =
+ {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
+  pri: int, interrupts: bool};
+
+fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   if null es then []
   else
     let
@@ -432,7 +437,7 @@
         | SOME grp => grp);
       fun enqueue e queue =
         let
-          val (result, job) = future_job grp e;
+          val (result, job) = future_job grp interrupts e;
           val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
           val future = Future {promised = false, task = task, result = result};
         in (future, queue') end;
@@ -447,7 +452,9 @@
         in futures end)
     end;
 
-fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
+fun fork_pri pri e =
+  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+
 fun fork e = fork_pri 0 e;
 
 
@@ -513,7 +520,7 @@
   let
     val task = task_of x;
     val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
-    val (result, job) = future_job group (fn () => f (join x));
+    val (result, job) = future_job group true (fn () => f (join x));
 
     val extended = SYNCHRONIZED "extend" (fn () =>
       (case Task_Queue.extend task job (! queue) of
@@ -523,8 +530,8 @@
     if extended then Future {promised = false, task = task, result = result}
     else
       singleton
-        (forks {name = "Future.map", group = SOME group,
-          deps = [task], pri = Task_Queue.pri_of_task task})
+        (forks {name = "Future.map", group = SOME group, deps = [task],
+          pri = Task_Queue.pri_of_task task, interrupts = true})
         (fn () => f (join x))
   end;
 

--- a/src/Pure/Concurrent/par_list.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -35,7 +35,7 @@
     let
       val group = Task_Queue.new_group (Future.worker_group ());
       val futures =
-        Future.forks {name = name, group = SOME group, deps = [], pri = 0}
+        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);

--- a/src/Pure/PIDE/document.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -228,7 +228,7 @@
   ignore
     (singleton
       (Future.forks {name = "Document.async_state",
-        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
+        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
       (fn () =>
         Toplevel.setmp_thread_position tr
           (fn () => Toplevel.print_state false st) ()));
@@ -359,7 +359,8 @@
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
       val execution' = (* FIXME proper node deps *)
-        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
+        Future.forks
+          {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
           [fn () =>
             node_names_of version |> List.app (fn name =>
               fold_entries NONE (fn (_, exec) => fn () => force_exec exec)

--- a/src/Pure/Syntax/syntax.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -489,7 +489,7 @@
 fun future_gram deps e =
   singleton
     (Future.cond_forks {name = "Syntax.gram", group = NONE,
-      deps = map Future.task_of deps, pri = 0}) e;
+      deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
 
 datatype syntax =
   Syntax of {

--- a/src/Pure/Thy/thy_info.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -205,7 +205,9 @@
 
             val future =
               singleton
-                (Future.forks {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0})
+                (Future.forks
+                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
+                    interrupts = true})
                 (fn () =>
                   (case map_filter failed deps of
                     [] => body (map (#1 o Future.join o get) parents)

--- a/src/Pure/Thy/thy_load.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -189,7 +189,7 @@
 
     val present =
       singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
-        deps = map Future.task_of results, pri = 0})
+        deps = map Future.task_of results, pri = 0, interrupts = true})
       (fn () =>
         Thy_Output.present_thy (#1 lexs) Keyword.command_tags
           (Outer_Syntax.is_markup outer_syntax)

--- a/src/Pure/goal.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/goal.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -124,7 +124,8 @@
     let
       val _ = forked 1;
       val future =
-        singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
+        singleton
+          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = true})
           (fn () =>
             (*interruptible*)
             Exn.release

--- a/src/Pure/proofterm.ML	Wed Aug 10 15:17:24 2011 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 10 16:05:14 2011 +0200
@@ -1404,7 +1404,8 @@
   | fulfill_proof_future thy promises postproc body =
       singleton
         (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
-            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
+            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+            interrupts = true})
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
 
@@ -1461,7 +1462,9 @@
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
         singleton
-          (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+          (Future.forks
+            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
+              interrupts = true})
           (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);