src/Pure/PIDE/markup.scala
changeset 51818 517f232e867d
parent 51662 3391a493f39a
child 52111 1fd184eaa310
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Apr 29 14:07:03 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Apr 29 15:47:42 2013 +0200
     1.3 @@ -218,18 +218,7 @@
     1.4  
     1.5    /* command timing */
     1.6  
     1.7 -  object Command_Timing
     1.8 -  {
     1.9 -    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
    1.10 -      props match {
    1.11 -        case (FUNCTION, "command_timing") :: args =>
    1.12 -          (args, args) match {
    1.13 -            case (Position.Id(id), Timing_Properties(timing)) => Some((id, timing))
    1.14 -            case _ => None
    1.15 -          }
    1.16 -        case _ => None
    1.17 -      }
    1.18 -  }
    1.19 +  val COMMAND_TIMING = "command_timing"
    1.20  
    1.21  
    1.22    /* toplevel */