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;
     1 /*  Title:      Pure/PIDE/markup.scala
     2     Module:     PIDE
     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 
    30 sealed case class Markup(name: String, properties: Properties.T)
    31