--- 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
}
}