src/Pure/PIDE/document.ML
changeset 41674 7da257539a8d
parent 41673 1c191a39549f
child 42012 2c3fe3cbebae
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Jan 31 22:57:01 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Jan 31 23:02:53 2011 +0100
     1.3 @@ -209,7 +209,7 @@
     1.4  fun async_state tr st =
     1.5    ignore
     1.6      (singleton
     1.7 -      (Future.bulk {name = "Document.async_state",
     1.8 +      (Future.forks {name = "Document.async_state",
     1.9          group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
    1.10        (fn () =>
    1.11          Toplevel.setmp_thread_position tr
    1.12 @@ -339,7 +339,7 @@
    1.13        val _ = cancel state;
    1.14  
    1.15        val execution' = (* FIXME proper node deps *)
    1.16 -        Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
    1.17 +        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
    1.18            [fn () =>
    1.19              let
    1.20                val _ = await_cancellation state;