# HG changeset patch
# User wenzelm
# Date 1313769683 -7200
# Node ID 0a1934c5c104930f8c387e339e483a7fd08b59a4
# Parent  65f60d9ac4bff4f026bed40d5f6762ab301524e7
tuned;

diff -r 65f60d9ac4bf -r 0a1934c5c104 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 19 17:39:37 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 19 18:01:23 2011 +0200
@@ -200,9 +200,10 @@
   map_state (fn (versions, commands, execs, execution) =>
     let
       val id_string = print_id id;
-      val tr = Future.fork_pri 2 (fn () =>
-        Position.setmp_thread_data (Position.id_only id_string)
-          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+      val tr =
+        Future.fork_pri 2 (fn () =>
+          Position.setmp_thread_data (Position.id_only id_string)
+            (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
       val commands' =
         Inttab.update_new (id, tr) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -251,14 +252,13 @@
   | NONE => ());
 
 fun async_state tr st =
-  ignore
-    (singleton
-      (Future.forks {name = "Document.async_state",
-        group = SOME (Future.new_group NONE),
-        deps = [], pri = 0, interrupts = true})
-      (fn () =>
-        Toplevel.setmp_thread_position tr
-          (fn () => Toplevel.print_state false st) ()));
+  (singleton o Future.forks)
+    {name = "Document.async_state", group = SOME (Future.new_group NONE),
+      deps = [], pri = 0, interrupts = true}
+    (fn () =>
+      Toplevel.setmp_thread_position tr
+        (fn () => Toplevel.print_state false st) ())
+  |> ignore;
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -354,9 +354,9 @@
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));
               in
-                singleton
-                  (Future.forks {name = "Document.edit", group = NONE,
-                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
+                (singleton o Future.forks)
+                  {name = "Document.edit", group = NONE,
+                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
                   (fn () =>
                     let
                       val prev_exec =
@@ -396,11 +396,9 @@
       val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
-            singleton
-              (Future.forks
-                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
-                  deps = map (Future.task_of o #2) deps,
-                  pri = 1, interrupts = true})
+            (singleton o Future.forks)
+              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
               (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
 
     in (versions, commands, execs, execution) end);
diff -r 65f60d9ac4bf -r 0a1934c5c104 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 19 17:39:37 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 19 18:01:23 2011 +0200
@@ -194,11 +194,9 @@
   Graph.schedule (fn deps => fn (name, task) =>
     (case task of
       Task (parents, body) =>
-        singleton
-          (Future.forks
-            {name = "theory:" ^ name, group = NONE,
-              deps = map (Future.task_of o #2) deps,
-              pri = 0, interrupts = true})
+        (singleton o Future.forks)
+          {name = "theory:" ^ name, group = NONE,
+            deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
           (fn () =>
             (case filter (not o can Future.join o #2) deps of
               [] => body (map (#1 o Future.join) (task_parents deps parents))
diff -r 65f60d9ac4bf -r 0a1934c5c104 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 19 17:39:37 2011 +0200
+++ b/src/Pure/goal.ML	Fri Aug 19 18:01:23 2011 +0200
@@ -124,8 +124,8 @@
     let
       val _ = forked 1;
       val future =
-        singleton
-          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
+        (singleton o Future.forks)
+          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
diff -r 65f60d9ac4bf -r 0a1934c5c104 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 19 17:39:37 2011 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 19 18:01:23 2011 +0200
@@ -1402,10 +1402,10 @@
       if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
       else Future.map postproc body
   | 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,
-            interrupts = true})
+      (singleton o Future.forks)
+        {name = "Proofterm.fulfill_proof_future", group = NONE,
+          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,10 +1461,9 @@
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
       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,
-              interrupts = true})
+        (singleton o 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);