src/Pure/PIDE/markup.scala
changeset 50255 d0ec1f0d1d7d
parent 50215 97959912840a
child 50450 358b6020f8b6
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Nov 28 16:09:05 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Nov 28 17:18:53 2012 +0100
     1.3 @@ -307,6 +307,15 @@
     1.4          case _ => None
     1.5        }
     1.6    }
     1.7 +
     1.8 +  object ML_Statistics
     1.9 +  {
    1.10 +    def unapply(props: Properties.T): Option[Properties.T] =
    1.11 +      props match {
    1.12 +        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
    1.13 +        case _ => None
    1.14 +      }
    1.15 +  }
    1.16  }
    1.17  
    1.18