diff -r 7957d26c3334 -r 3f6280aedbcc src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 25 20:00:27 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Mar 26 11:26:13 2013 +0100
@@ -116,6 +116,36 @@
   }
 
 
+  /* node timing */
+
+  sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
+
+  val empty_node_timing = Node_Timing(0.0, Map.empty)
+
+  def node_timing(
+    state: Document.State,
+    version: Document.Version,
+    node: Document.Node,
+    threshold: Double): Node_Timing =
+  {
+    var total = 0.0
+    var commands = Map.empty[Command, Double]
+    for {
+      command <- node.commands.iterator
+      st = state.command_state(version, command)
+      command_timing =
+        (0.0 /: st.status)({
+          case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
+          case (timing, _) => timing
+        })
+    } {
+      total += command_timing
+      if (command_timing >= threshold) commands += (command -> command_timing)
+    }
+    Node_Timing(total, commands)
+  }
+
+
   /* result messages */
 
   private val clean = Set(Markup.REPORT, Markup.NO_REPORT)