tuned;
authorwenzelm
Fri Aug 19 18:01:23 2011 +0200 (2011-08-19 ago)
changeset 443020a1934c5c104
parent 44301 65f60d9ac4bf
child 44303 4e2abb045eac
tuned;
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/goal.ML
src/Pure/proofterm.ML
     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);