# HG changeset patch
# User wenzelm
# Date 1375194127 -7200
# Node ID 0d6f2a87d1a58618557cc6b06b22ff6296443131
# Parent  ad64ed8e614772ced146ac29aabe92a371d96ee9
more timing;

diff -r ad64ed8e6147 -r 0d6f2a87d1a5 src/Pure/PIDE/document.ML
--- 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;