src/Pure/PIDE/markup.scala
changeset 56548 ae6870efc28d
parent 56278 2576d3a40ed6
child 56616 abc2da18d08d
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 11 23:26:31 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 12 17:46:54 2014 +0200
     1.3 @@ -137,7 +137,9 @@
     1.4    val SEPARATOR = "separator"
     1.5  
     1.6  
     1.7 -  /* hidden text */
     1.8 +  /* text properties */
     1.9 +
    1.10 +  val WORDS = "words"
    1.11  
    1.12    val HIDDEN = "hidden"
    1.13