clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
authorwenzelm
Mon Apr 29 15:47:42 2013 +0200 (2013-04-29 ago)
changeset 51818517f232e867d
parent 51817 6b82042690b5
child 51819 9df935196be9
child 51820 142c69695785
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
     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 */
     2.1 --- a/src/Pure/PIDE/protocol.scala	Mon Apr 29 14:07:03 2013 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Apr 29 15:47:42 2013 +0200
     2.3 @@ -84,6 +84,22 @@
     2.4      (Status.init /: markups)(command_status(_, _))
     2.5  
     2.6  
     2.7 +  /* command timing */
     2.8 +
     2.9 +  object Command_Timing
    2.10 +  {
    2.11 +    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
    2.12 +      props match {
    2.13 +        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
    2.14 +          (args, args) match {
    2.15 +            case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
    2.16 +            case _ => None
    2.17 +          }
    2.18 +        case _ => None
    2.19 +      }
    2.20 +  }
    2.21 +
    2.22 +
    2.23    /* node status */
    2.24  
    2.25    sealed case class Node_Status(
     3.1 --- a/src/Pure/System/session.scala	Mon Apr 29 14:07:03 2013 +0200
     3.2 +++ b/src/Pure/System/session.scala	Mon Apr 29 15:47:42 2013 +0200
     3.3 @@ -322,7 +322,7 @@
     3.4          case Position.Id(state_id) if !output.is_protocol =>
     3.5            accumulate(state_id, output.message)
     3.6  
     3.7 -        case Markup.Command_Timing(state_id, timing) if output.is_protocol =>
     3.8 +        case Protocol.Command_Timing(state_id, timing) if output.is_protocol =>
     3.9            val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
    3.10            accumulate(state_id, prover.get.xml_cache.elem(message))
    3.11