src/Pure/PIDE/markup.scala
author wenzelm
Tue Nov 29 19:49:36 2011 +0100 (2011-11-29 ago)
changeset 45670 b84170538043
parent 45667 src/Pure/General/markup.scala@546d78f0d81f
child 45673 cd41e3903fbf
permissions -rw-r--r--
rearranged files;
     1 /*  Title:      Pure/PIDE/markup.scala
     2     Module:     Library
     3     Author:     Makarius
     4 
     5 Generic markup elements.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 object Markup
    12 {
    13   /* properties */
    14 
    15   val NAME = "name"
    16   val Name = new Properties.String(NAME)
    17 
    18   val KIND = "kind"
    19   val Kind = new Properties.String(KIND)
    20 
    21 
    22   /* elements */
    23 
    24   val Empty = Markup("", Nil)
    25   val Data = Markup("data", Nil)
    26   val Broken = Markup("broken", Nil)
    27 
    28 
    29   /* timing */
    30 
    31   val TIMING = "timing"
    32   val ELAPSED = "elapsed"
    33   val CPU = "cpu"
    34   val GC = "gc"
    35 
    36   object Timing
    37   {
    38     def apply(timing: isabelle.Timing): Markup =
    39       Markup(TIMING, List(
    40         (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
    41         (CPU, Properties.Value.Double(timing.cpu.seconds)),
    42         (GC, Properties.Value.Double(timing.gc.seconds))))
    43     def unapply(markup: Markup): Option[isabelle.Timing] =
    44       markup match {
    45         case Markup(TIMING, List(
    46           (ELAPSED, Properties.Value.Double(elapsed)),
    47           (CPU, Properties.Value.Double(cpu)),
    48           (GC, Properties.Value.Double(gc)))) =>
    49             Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    50         case _ => None
    51       }
    52   }
    53 }
    54 
    55 
    56 sealed case class Markup(name: String, properties: Properties.T)
    57