src/Pure/PIDE/markup.scala
changeset 45670 b84170538043
parent 45667 546d78f0d81f
child 45673 cd41e3903fbf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Nov 29 19:49:36 2011 +0100
     1.3 @@ -0,0 +1,57 @@
     1.4 +/*  Title:      Pure/PIDE/markup.scala
     1.5 +    Module:     Library
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Generic markup elements.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +object Markup
    1.15 +{
    1.16 +  /* properties */
    1.17 +
    1.18 +  val NAME = "name"
    1.19 +  val Name = new Properties.String(NAME)
    1.20 +
    1.21 +  val KIND = "kind"
    1.22 +  val Kind = new Properties.String(KIND)
    1.23 +
    1.24 +
    1.25 +  /* elements */
    1.26 +
    1.27 +  val Empty = Markup("", Nil)
    1.28 +  val Data = Markup("data", Nil)
    1.29 +  val Broken = Markup("broken", Nil)
    1.30 +
    1.31 +
    1.32 +  /* timing */
    1.33 +
    1.34 +  val TIMING = "timing"
    1.35 +  val ELAPSED = "elapsed"
    1.36 +  val CPU = "cpu"
    1.37 +  val GC = "gc"
    1.38 +
    1.39 +  object Timing
    1.40 +  {
    1.41 +    def apply(timing: isabelle.Timing): Markup =
    1.42 +      Markup(TIMING, List(
    1.43 +        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    1.44 +        (CPU, Properties.Value.Double(timing.cpu.seconds)),
    1.45 +        (GC, Properties.Value.Double(timing.gc.seconds))))
    1.46 +    def unapply(markup: Markup): Option[isabelle.Timing] =
    1.47 +      markup match {
    1.48 +        case Markup(TIMING, List(
    1.49 +          (ELAPSED, Properties.Value.Double(elapsed)),
    1.50 +          (CPU, Properties.Value.Double(cpu)),
    1.51 +          (GC, Properties.Value.Double(gc)))) =>
    1.52 +            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    1.53 +        case _ => None
    1.54 +      }
    1.55 +  }
    1.56 +}
    1.57 +
    1.58 +
    1.59 +sealed case class Markup(name: String, properties: Properties.T)
    1.60 +