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