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;
wenzelm@45670
     1
/*  Title:      Pure/PIDE/markup.scala
wenzelm@45667
     2
    Module:     Library
wenzelm@27958
     3
    Author:     Makarius
wenzelm@27958
     4
wenzelm@45666
     5
Generic markup elements.
wenzelm@27958
     6
*/
wenzelm@27958
     7
wenzelm@27958
     8
package isabelle
wenzelm@27958
     9
wenzelm@27970
    10
wenzelm@32450
    11
object Markup
wenzelm@32450
    12
{
wenzelm@45666
    13
  /* properties */
wenzelm@29184
    14
wenzelm@29184
    15
  val NAME = "name"
wenzelm@43780
    16
  val Name = new Properties.String(NAME)
wenzelm@42136
    17
wenzelm@29184
    18
  val KIND = "kind"
wenzelm@43780
    19
  val Kind = new Properties.String(KIND)
wenzelm@29184
    20
wenzelm@29184
    21
wenzelm@45666
    22
  /* elements */
wenzelm@29184
    23
wenzelm@45666
    24
  val Empty = Markup("", Nil)
wenzelm@45666
    25
  val Data = Markup("data", Nil)
wenzelm@45666
    26
  val Broken = Markup("broken", Nil)
wenzelm@43673
    27
wenzelm@43673
    28
wenzelm@40394
    29
  /* timing */
wenzelm@40394
    30
wenzelm@40394
    31
  val TIMING = "timing"
wenzelm@40394
    32
  val ELAPSED = "elapsed"
wenzelm@40394
    33
  val CPU = "cpu"
wenzelm@40394
    34
  val GC = "gc"
wenzelm@40394
    35
wenzelm@40394
    36
  object Timing
wenzelm@40394
    37
  {
wenzelm@40394
    38
    def apply(timing: isabelle.Timing): Markup =
wenzelm@40394
    39
      Markup(TIMING, List(
wenzelm@43780
    40
        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
wenzelm@43780
    41
        (CPU, Properties.Value.Double(timing.cpu.seconds)),
wenzelm@43780
    42
        (GC, Properties.Value.Double(timing.gc.seconds))))
wenzelm@40394
    43
    def unapply(markup: Markup): Option[isabelle.Timing] =
wenzelm@40394
    44
      markup match {
wenzelm@40394
    45
        case Markup(TIMING, List(
wenzelm@43780
    46
          (ELAPSED, Properties.Value.Double(elapsed)),
wenzelm@43780
    47
          (CPU, Properties.Value.Double(cpu)),
wenzelm@43780
    48
          (GC, Properties.Value.Double(gc)))) =>
wenzelm@40848
    49
            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
wenzelm@40394
    50
        case _ => None
wenzelm@40394
    51
      }
wenzelm@40394
    52
  }
wenzelm@45666
    53
}
wenzelm@43721
    54
wenzelm@43721
    55
wenzelm@45666
    56
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
    57