# HG changeset patch
# User wenzelm
# Date 1508156474 -7200
# Node ID 69afe45a6062978755ff78ea468b05e93c519d85
# Parent  a804fa68f62cb7e0beece9067925bd977529cad4
tuned;

diff -r a804fa68f62c -r 69afe45a6062 src/Pure/PIDE/markup.scala
--- 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
       }
   }