src/Pure/PIDE/markup.scala
changeset 66872 69afe45a6062
parent 66382 6392766f3c25
child 66873 9953ae603a23
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 16 11:37:14 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 16 14:21:14 2017 +0200
     1.3 @@ -540,7 +540,7 @@
     1.4    {
     1.5      def unapply(props: Properties.T): Option[Properties.T] =
     1.6        props match {
     1.7 -        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
     1.8 +        case (FUNCTION, "ML_statistics") :: props => Some(props)
     1.9          case _ => None
    1.10        }
    1.11    }
    1.12 @@ -549,7 +549,7 @@
    1.13    {
    1.14      def unapply(props: Properties.T): Option[Properties.T] =
    1.15        props match {
    1.16 -        case (FUNCTION, "task_statistics") :: stats => Some(stats)
    1.17 +        case (FUNCTION, "task_statistics") :: props => Some(props)
    1.18          case _ => None
    1.19        }
    1.20    }