src/Pure/PIDE/markup.scala
changeset 65937 fde7b5d209d5
parent 65753 787e5ee6ef53
child 66044 bd7516709051
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri May 26 19:39:02 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri May 26 20:52:01 2017 +0200
     1.3 @@ -43,6 +43,9 @@
     1.4    val KIND = "kind"
     1.5    val Kind = new Properties.String(KIND)
     1.6  
     1.7 +  val CONTENT = "content"
     1.8 +  val Content = new Properties.String(CONTENT)
     1.9 +
    1.10    val SERIAL = "serial"
    1.11    val Serial = new Properties.Long(SERIAL)
    1.12