--- a/src/Pure/PIDE/document.ML Tue Jul 30 16:01:19 2013 +0200
+++ b/src/Pure/PIDE/document.ML Tue Jul 30 16:22:07 2013 +0200
@@ -472,7 +472,7 @@
(singleton o Future.forks)
{name = "Document.update", group = NONE,
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
- (fn () =>
+ (fn () => timeit ("Document.update " ^ name) (fn () =>
let
val imports = map (apsnd Future.join) deps;
val imports_result_changed = exists (#4 o #1 o #2) imports;
@@ -525,7 +525,7 @@
val result_changed = changed_result node0 node';
in ((removed, assign_update, assigned_node, result_changed), node') end
else (([], [], NONE, false), node)
- end))
+ end)))
|> Future.joins |> map #1);
val removed = maps #1 updated;