src/Pure/PIDE/protocol.scala
changeset 66873 9953ae603a23
parent 66717 67dbf5cdc056
child 67219 81e9804b2014
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4    {
     1.5      def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
     1.6        props match {
     1.7 -        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
     1.8 +        case Markup.COMMAND_TIMING :: args =>
     1.9            (args, args) match {
    1.10              case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
    1.11              case _ => None
    1.12 @@ -123,6 +123,22 @@
    1.13    }
    1.14  
    1.15  
    1.16 +  /* theory timing */
    1.17 +
    1.18 +  object Theory_Timing
    1.19 +  {
    1.20 +    def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
    1.21 +      props match {
    1.22 +        case Markup.THEORY_TIMING :: args =>
    1.23 +          (args, args) match {
    1.24 +            case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
    1.25 +            case _ => None
    1.26 +          }
    1.27 +        case _ => None
    1.28 +      }
    1.29 +  }
    1.30 +
    1.31 +
    1.32    /* node status */
    1.33  
    1.34    sealed case class Node_Status(