changeset 44247 | 270366301bd7 |
parent 44226 | 1ea760da0f2d |
child 44270 | 3eaad39e520c |
--- a/src/Pure/PIDE/document.ML Wed Aug 17 20:08:36 2011 +0200 +++ b/src/Pure/PIDE/document.ML Wed Aug 17 22:14:22 2011 +0200 @@ -372,7 +372,7 @@ |> set_result result; in ((assigns, execs, [(name, node')]), node') end) end)) - |> Future.join_results |> Exn.release_all |> map #1; + |> Future.join_results |> Par_Exn.release_all |> map #1; val state' = state |> fold (fold define_exec o #2) updates