changeset 44330 | b28e091f683a |
parent 44302 | 0a1934c5c104 |
child 44338 | 700008399ee5 |
--- a/src/Pure/PIDE/document.ML Sat Aug 20 09:42:34 2011 +0200 +++ b/src/Pure/PIDE/document.ML Sat Aug 20 15:52:29 2011 +0200 @@ -371,7 +371,7 @@ |> set_result result; in ((assigns, execs, [(name, node')]), node') end) end)) - |> Future.join_results |> Par_Exn.release_all |> map #1; + |> Future.joins |> map #1; val state' = state |> fold (fold define_exec o #2) updates