src/Pure/PIDE/markup.scala
author wenzelm
Tue Nov 29 21:50:00 2011 +0100 (2011-11-29 ago)
changeset 45674 eb65c9d17e2f
parent 45673 cd41e3903fbf
child 49613 2f6986e2ef06
permissions -rw-r--r--
clarified Time vs. Timing;
wenzelm@45670
     1
/*  Title:      Pure/PIDE/markup.scala
wenzelm@45673
     2
    Module:     PIDE
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@45666
    27
}
wenzelm@43721
    28
wenzelm@43721
    29
wenzelm@45666
    30
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
    31