diff -r 55f8bd61b029 -r 73ec6ad6700e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 18 16:20:09 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 18 17:51:50 2013 +0100
@@ -330,6 +330,15 @@
         case _ => None
       }
   }
+
+  object Task_Statistics
+  {
+    def unapply(props: Properties.T): Option[Properties.T] =
+      props match {
+        case (FUNCTION, "task_statistics") :: stats => Some(stats)
+        case _ => None
+      }
+  }
 }