src/Pure/PIDE/markup.scala
changeset 68997 4278947ba336
parent 68884 9b97d0b20d95
child 69320 fc221fa79741
     1.1 --- a/src/Pure/PIDE/markup.scala	Sun Sep 02 22:30:08 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Sep 15 23:35:46 2018 +0200
     1.3 @@ -40,6 +40,9 @@
     1.4    val NAME = "name"
     1.5    val Name = new Properties.String(NAME)
     1.6  
     1.7 +  val XNAME = "xname"
     1.8 +  val XName = new Properties.String(XNAME)
     1.9 +
    1.10    val KIND = "kind"
    1.11    val Kind = new Properties.String(KIND)
    1.12