src/Pure/PIDE/document.ML
changeset 41630 a7a93df23664
parent 41629 5490dc4d999d
child 41634 28d94383249c
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Jan 25 20:06:32 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jan 25 21:26:25 2011 +0100
     1.3 @@ -328,11 +328,14 @@
     1.4        fun await_cancellation () = Future.join_results execution;
     1.5  
     1.6        val execution' = (* FIXME proper node deps *)
     1.7 -        node_names_of version |> map (fn name =>
     1.8 -          Future.fork_pri 1 (fn () =>
     1.9 -            (await_cancellation ();
    1.10 -              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.11 -                (get_node version name) ())));
    1.12 +        [Future.fork_pri 1 (fn () =>
    1.13 +          let
    1.14 +            val _ = await_cancellation ();
    1.15 +            val _ =
    1.16 +              node_names_of version |> List.app (fn name =>
    1.17 +                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.18 +                    (get_node version name) ());
    1.19 +          in () end)];
    1.20  
    1.21        val _ = await_cancellation ();
    1.22