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