src/Pure/PIDE/markup.scala
author wenzelm
Thu Sep 27 15:55:38 2012 +0200 (2012-09-27 ago)
changeset 49613 2f6986e2ef06
parent 45674 eb65c9d17e2f
child 50201 c26369c9eda6
permissions -rw-r--r--
removed obsolete org.w3c.dom operations;
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 Broken = Markup("broken", Nil)
wenzelm@45666
    26
}
wenzelm@43721
    27
wenzelm@43721
    28
wenzelm@45666
    29
sealed case class Markup(name: String, properties: Properties.T)
wenzelm@43748
    30