src/Pure/PIDE/document.ML
changeset 41673 1c191a39549f
parent 41672 2f70b1ddd09f
child 41674 7da257539a8d
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jan 31 21:54:49 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jan 31 22:57:01 2011 +0100
     1.3 @@ -208,7 +208,9 @@
     1.4  
     1.5  fun async_state tr st =
     1.6    ignore
     1.7 -    (singleton (Future.bulk {group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
     1.8 +    (singleton
     1.9 +      (Future.bulk {name = "Document.async_state",
    1.10 +        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
    1.11        (fn () =>
    1.12          Toplevel.setmp_thread_position tr
    1.13            (fn () => Toplevel.print_state false st) ()));
    1.14 @@ -327,7 +329,7 @@
    1.15  (* execute *)
    1.16  
    1.17  fun execute version_id state =
    1.18 -  state |> map_state (fn (versions, commands, execs, execution) =>
    1.19 +  state |> map_state (fn (versions, commands, execs, _) =>
    1.20      let
    1.21        val version = the_version state version_id;
    1.22  
    1.23 @@ -337,14 +339,15 @@
    1.24        val _ = cancel state;
    1.25  
    1.26        val execution' = (* FIXME proper node deps *)
    1.27 -        Future.bulk {group = NONE, deps = [], pri = 1} [fn () =>
    1.28 -          let
    1.29 -            val _ = await_cancellation state;
    1.30 -            val _ =
    1.31 -              node_names_of version |> List.app (fn name =>
    1.32 -                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.33 -                    (get_node version name) ());
    1.34 -          in () end];
    1.35 +        Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
    1.36 +          [fn () =>
    1.37 +            let
    1.38 +              val _ = await_cancellation state;
    1.39 +              val _ =
    1.40 +                node_names_of version |> List.app (fn name =>
    1.41 +                  fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
    1.42 +                      (get_node version name) ());
    1.43 +            in () end];
    1.44  
    1.45        val _ = await_cancellation state;  (* FIXME async!? *)
    1.46