src/Pure/PIDE/markup.scala
changeset 58048 aa6296d09e0e
parent 57598 e2305b9d1534
child 58464 5e7fc9974aba
     1.1 --- a/src/Pure/PIDE/markup.scala	Wed Aug 27 12:32:42 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Wed Aug 27 14:54:32 2014 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4    val HIDDEN = "hidden"
     1.5  
     1.6  
     1.7 -  /* logical entities */
     1.8 +  /* misc entities */
     1.9  
    1.10    val CLASS = "class"
    1.11    val TYPE_NAME = "type_name"