changeset 68997 | 4278947ba336 |
parent 68884 | 9b97d0b20d95 |
child 69320 | fc221fa79741 |
--- a/src/Pure/PIDE/markup.scala Sat Sep 15 22:33:48 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Sep 15 23:35:46 2018 +0200 @@ -40,6 +40,9 @@ val NAME = "name" val Name = new Properties.String(NAME) + val XNAME = "xname" + val XName = new Properties.String(XNAME) + val KIND = "kind" val Kind = new Properties.String(KIND)