future_job: explicit indication of interrupts;
authorwenzelm
Wed Aug 10 16:05:14 2011 +0200 (2011-08-10 ago)
changeset 441130baa8bbd355a
parent 44112 ef876972fdc1
child 44114 64634a9ecd46
future_job: explicit indication of interrupts;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/PIDE/document.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/goal.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 10 15:17:24 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 16:05:14 2011 +0200
     1.3 @@ -41,9 +41,10 @@
     1.4    val is_finished: 'a future -> bool
     1.5    val cancel_group: Task_Queue.group -> unit
     1.6    val cancel: 'a future -> unit
     1.7 -  val forks:
     1.8 -    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
     1.9 -      (unit -> 'a) list -> 'a future list
    1.10 +  type fork_params =
    1.11 +   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
    1.12 +    pri: int, interrupts: bool}
    1.13 +  val forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.14    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.15    val fork: (unit -> 'a) -> 'a future
    1.16    val join_results: 'a future list -> 'a Exn.result list
    1.17 @@ -51,9 +52,7 @@
    1.18    val join: 'a future -> 'a
    1.19    val value: 'a -> 'a future
    1.20    val map: ('a -> 'b) -> 'a future -> 'b future
    1.21 -  val cond_forks:
    1.22 -    {name: string, group: Task_Queue.group option, deps: Task_Queue.task list, pri: int} ->
    1.23 -      (unit -> 'a) list -> 'a future list
    1.24 +  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.25    val promise_group: Task_Queue.group -> 'a future
    1.26    val promise: unit -> 'a future
    1.27    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.28 @@ -403,7 +402,7 @@
    1.29        | Exn.Res _ => true);
    1.30    in ok end;
    1.31  
    1.32 -fun future_job group (e: unit -> 'a) =
    1.33 +fun future_job group interrupts (e: unit -> 'a) =
    1.34    let
    1.35      val result = Single_Assignment.var "future" : 'a result;
    1.36      val pos = Position.thread_data ();
    1.37 @@ -412,7 +411,9 @@
    1.38          val res =
    1.39            if ok then
    1.40              Exn.capture (fn () =>
    1.41 -              Multithreading.with_attributes Multithreading.private_interrupts
    1.42 +              Multithreading.with_attributes
    1.43 +                (if interrupts
    1.44 +                 then Multithreading.private_interrupts else Multithreading.no_interrupts)
    1.45                  (fn _ => Position.setmp_thread_data pos e ()) before
    1.46                Multithreading.interrupted ()) ()
    1.47            else Exn.interrupt_exn;
    1.48 @@ -422,7 +423,11 @@
    1.49  
    1.50  (* fork *)
    1.51  
    1.52 -fun forks {name, group, deps, pri} es =
    1.53 +type fork_params =
    1.54 + {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
    1.55 +  pri: int, interrupts: bool};
    1.56 +
    1.57 +fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
    1.58    if null es then []
    1.59    else
    1.60      let
    1.61 @@ -432,7 +437,7 @@
    1.62          | SOME grp => grp);
    1.63        fun enqueue e queue =
    1.64          let
    1.65 -          val (result, job) = future_job grp e;
    1.66 +          val (result, job) = future_job grp interrupts e;
    1.67            val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.68            val future = Future {promised = false, task = task, result = result};
    1.69          in (future, queue') end;
    1.70 @@ -447,7 +452,9 @@
    1.71          in futures end)
    1.72      end;
    1.73  
    1.74 -fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
    1.75 +fun fork_pri pri e =
    1.76 +  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
    1.77 +
    1.78  fun fork e = fork_pri 0 e;
    1.79  
    1.80  
    1.81 @@ -513,7 +520,7 @@
    1.82    let
    1.83      val task = task_of x;
    1.84      val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
    1.85 -    val (result, job) = future_job group (fn () => f (join x));
    1.86 +    val (result, job) = future_job group true (fn () => f (join x));
    1.87  
    1.88      val extended = SYNCHRONIZED "extend" (fn () =>
    1.89        (case Task_Queue.extend task job (! queue) of
    1.90 @@ -523,8 +530,8 @@
    1.91      if extended then Future {promised = false, task = task, result = result}
    1.92      else
    1.93        singleton
    1.94 -        (forks {name = "Future.map", group = SOME group,
    1.95 -          deps = [task], pri = Task_Queue.pri_of_task task})
    1.96 +        (forks {name = "Future.map", group = SOME group, deps = [task],
    1.97 +          pri = Task_Queue.pri_of_task task, interrupts = true})
    1.98          (fn () => f (join x))
    1.99    end;
   1.100  
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Wed Aug 10 15:17:24 2011 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Wed Aug 10 16:05:14 2011 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4      let
     2.5        val group = Task_Queue.new_group (Future.worker_group ());
     2.6        val futures =
     2.7 -        Future.forks {name = name, group = SOME group, deps = [], pri = 0}
     2.8 +        Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
     2.9            (map (fn x => fn () => f x) xs);
    2.10        val results = Future.join_results futures
    2.11          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     3.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 10 15:17:24 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 10 16:05:14 2011 +0200
     3.3 @@ -228,7 +228,7 @@
     3.4    ignore
     3.5      (singleton
     3.6        (Future.forks {name = "Document.async_state",
     3.7 -        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
     3.8 +        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
     3.9        (fn () =>
    3.10          Toplevel.setmp_thread_position tr
    3.11            (fn () => Toplevel.print_state false st) ()));
    3.12 @@ -359,7 +359,8 @@
    3.13          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
    3.14  
    3.15        val execution' = (* FIXME proper node deps *)
    3.16 -        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
    3.17 +        Future.forks
    3.18 +          {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
    3.19            [fn () =>
    3.20              node_names_of version |> List.app (fn name =>
    3.21                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
     4.1 --- a/src/Pure/Syntax/syntax.ML	Wed Aug 10 15:17:24 2011 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Aug 10 16:05:14 2011 +0200
     4.3 @@ -489,7 +489,7 @@
     4.4  fun future_gram deps e =
     4.5    singleton
     4.6      (Future.cond_forks {name = "Syntax.gram", group = NONE,
     4.7 -      deps = map Future.task_of deps, pri = 0}) e;
     4.8 +      deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
     4.9  
    4.10  datatype syntax =
    4.11    Syntax of {
     5.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 10 15:17:24 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 10 16:05:14 2011 +0200
     5.3 @@ -205,7 +205,9 @@
     5.4  
     5.5              val future =
     5.6                singleton
     5.7 -                (Future.forks {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0})
     5.8 +                (Future.forks
     5.9 +                  {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
    5.10 +                    interrupts = true})
    5.11                  (fn () =>
    5.12                    (case map_filter failed deps of
    5.13                      [] => body (map (#1 o Future.join o get) parents)
     6.1 --- a/src/Pure/Thy/thy_load.ML	Wed Aug 10 15:17:24 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Aug 10 16:05:14 2011 +0200
     6.3 @@ -189,7 +189,7 @@
     6.4  
     6.5      val present =
     6.6        singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
     6.7 -        deps = map Future.task_of results, pri = 0})
     6.8 +        deps = map Future.task_of results, pri = 0, interrupts = true})
     6.9        (fn () =>
    6.10          Thy_Output.present_thy (#1 lexs) Keyword.command_tags
    6.11            (Outer_Syntax.is_markup outer_syntax)
     7.1 --- a/src/Pure/goal.ML	Wed Aug 10 15:17:24 2011 +0200
     7.2 +++ b/src/Pure/goal.ML	Wed Aug 10 16:05:14 2011 +0200
     7.3 @@ -124,7 +124,8 @@
     7.4      let
     7.5        val _ = forked 1;
     7.6        val future =
     7.7 -        singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
     7.8 +        singleton
     7.9 +          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = true})
    7.10            (fn () =>
    7.11              (*interruptible*)
    7.12              Exn.release
     8.1 --- a/src/Pure/proofterm.ML	Wed Aug 10 15:17:24 2011 +0200
     8.2 +++ b/src/Pure/proofterm.ML	Wed Aug 10 16:05:14 2011 +0200
     8.3 @@ -1404,7 +1404,8 @@
     8.4    | fulfill_proof_future thy promises postproc body =
     8.5        singleton
     8.6          (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
     8.7 -            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
     8.8 +            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
     8.9 +            interrupts = true})
    8.10          (fn () =>
    8.11            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    8.12  
    8.13 @@ -1461,7 +1462,9 @@
    8.14        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    8.15        else
    8.16          singleton
    8.17 -          (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
    8.18 +          (Future.forks
    8.19 +            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
    8.20 +              interrupts = true})
    8.21            (make_body0 o full_proof0);
    8.22  
    8.23      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);