author | wenzelm |
Sun, 20 May 2012 11:34:33 +0200 | |
changeset 47884 | 21c42b095c84 |
parent 45674 | eb65c9d17e2f |
child 49613 | 2f6986e2ef06 |
permissions | -rw-r--r-- |
/* Title: Pure/PIDE/markup.scala Module: PIDE Author: Makarius Generic markup elements. */ package isabelle object Markup { /* properties */ val NAME = "name" val Name = new Properties.String(NAME) val KIND = "kind" val Kind = new Properties.String(KIND) /* elements */ val Empty = Markup("", Nil) val Data = Markup("data", Nil) val Broken = Markup("broken", Nil) } sealed case class Markup(name: String, properties: Properties.T)