1.1 --- a/src/Pure/PIDE/document.ML Fri Aug 19 17:39:37 2011 +0200
1.2 +++ b/src/Pure/PIDE/document.ML Fri Aug 19 18:01:23 2011 +0200
1.3 @@ -200,9 +200,10 @@
1.4 map_state (fn (versions, commands, execs, execution) =>
1.5 let
1.6 val id_string = print_id id;
1.7 - val tr = Future.fork_pri 2 (fn () =>
1.8 - Position.setmp_thread_data (Position.id_only id_string)
1.9 - (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
1.10 + val tr =
1.11 + Future.fork_pri 2 (fn () =>
1.12 + Position.setmp_thread_data (Position.id_only id_string)
1.13 + (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
1.14 val commands' =
1.15 Inttab.update_new (id, tr) commands
1.16 handle Inttab.DUP dup => err_dup "command" dup;
1.17 @@ -251,14 +252,13 @@
1.18 | NONE => ());
1.19
1.20 fun async_state tr st =
1.21 - ignore
1.22 - (singleton
1.23 - (Future.forks {name = "Document.async_state",
1.24 - group = SOME (Future.new_group NONE),
1.25 - deps = [], pri = 0, interrupts = true})
1.26 - (fn () =>
1.27 - Toplevel.setmp_thread_position tr
1.28 - (fn () => Toplevel.print_state false st) ()));
1.29 + (singleton o Future.forks)
1.30 + {name = "Document.async_state", group = SOME (Future.new_group NONE),
1.31 + deps = [], pri = 0, interrupts = true}
1.32 + (fn () =>
1.33 + Toplevel.setmp_thread_position tr
1.34 + (fn () => Toplevel.print_state false st) ())
1.35 + |> ignore;
1.36
1.37 fun run int tr st =
1.38 (case Toplevel.transition int tr st of
1.39 @@ -354,9 +354,9 @@
1.40 fun get_command id =
1.41 (id, the_command state id |> Future.map (Toplevel.modify_init init));
1.42 in
1.43 - singleton
1.44 - (Future.forks {name = "Document.edit", group = NONE,
1.45 - deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
1.46 + (singleton o Future.forks)
1.47 + {name = "Document.edit", group = NONE,
1.48 + deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
1.49 (fn () =>
1.50 let
1.51 val prev_exec =
1.52 @@ -396,11 +396,9 @@
1.53 val _ =
1.54 nodes_of version |> Graph.schedule
1.55 (fn deps => fn (name, node) =>
1.56 - singleton
1.57 - (Future.forks
1.58 - {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
1.59 - deps = map (Future.task_of o #2) deps,
1.60 - pri = 1, interrupts = true})
1.61 + (singleton o Future.forks)
1.62 + {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
1.63 + deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
1.64 (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
1.65
1.66 in (versions, commands, execs, execution) end);
2.1 --- a/src/Pure/Thy/thy_info.ML Fri Aug 19 17:39:37 2011 +0200
2.2 +++ b/src/Pure/Thy/thy_info.ML Fri Aug 19 18:01:23 2011 +0200
2.3 @@ -194,11 +194,9 @@
2.4 Graph.schedule (fn deps => fn (name, task) =>
2.5 (case task of
2.6 Task (parents, body) =>
2.7 - singleton
2.8 - (Future.forks
2.9 - {name = "theory:" ^ name, group = NONE,
2.10 - deps = map (Future.task_of o #2) deps,
2.11 - pri = 0, interrupts = true})
2.12 + (singleton o Future.forks)
2.13 + {name = "theory:" ^ name, group = NONE,
2.14 + deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
2.15 (fn () =>
2.16 (case filter (not o can Future.join o #2) deps of
2.17 [] => body (map (#1 o Future.join) (task_parents deps parents))
3.1 --- a/src/Pure/goal.ML Fri Aug 19 17:39:37 2011 +0200
3.2 +++ b/src/Pure/goal.ML Fri Aug 19 18:01:23 2011 +0200
3.3 @@ -124,8 +124,8 @@
3.4 let
3.5 val _ = forked 1;
3.6 val future =
3.7 - singleton
3.8 - (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
3.9 + (singleton o Future.forks)
3.10 + {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
3.11 (fn () =>
3.12 Exn.release
3.13 (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
4.1 --- a/src/Pure/proofterm.ML Fri Aug 19 17:39:37 2011 +0200
4.2 +++ b/src/Pure/proofterm.ML Fri Aug 19 18:01:23 2011 +0200
4.3 @@ -1402,10 +1402,10 @@
4.4 if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
4.5 else Future.map postproc body
4.6 | fulfill_proof_future thy promises postproc body =
4.7 - singleton
4.8 - (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
4.9 - deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
4.10 - interrupts = true})
4.11 + (singleton o Future.forks)
4.12 + {name = "Proofterm.fulfill_proof_future", group = NONE,
4.13 + deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
4.14 + interrupts = true}
4.15 (fn () =>
4.16 postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
4.17
4.18 @@ -1461,10 +1461,9 @@
4.19 if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
4.20 else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
4.21 else
4.22 - singleton
4.23 - (Future.forks
4.24 - {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
4.25 - interrupts = true})
4.26 + (singleton o Future.forks)
4.27 + {name = "Proofterm.prepare_thm_proof", group = NONE,
4.28 + deps = [], pri = ~1, interrupts = true}
4.29 (make_body0 o full_proof0);
4.30
4.31 fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);