tuned;

--- a/src/Pure/PIDE/markup.scala	Mon Oct 16 11:37:14 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 16 14:21:14 2017 +0200
@@ -540,7 +540,7 @@
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
-        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
+        case (FUNCTION, "ML_statistics") :: props => Some(props)
         case _ => None
       }
   }
@@ -549,7 +549,7 @@
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
-        case (FUNCTION, "task_statistics") :: stats => Some(stats)
+        case (FUNCTION, "task_statistics") :: props => Some(props)
         case _ => None
       }
   }