src/Pure/PIDE/markup.scala
changeset 68298 2c3ce27cf4a8
parent 68148 fb661e4c4717
child 68323 bf7336731981
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat May 26 22:12:18 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sun May 27 13:42:01 2018 +0200
     1.3 @@ -242,6 +242,8 @@
     1.4  
     1.5    val HIDDEN = "hidden"
     1.6  
     1.7 +  val DELETE = "delete"
     1.8 +
     1.9  
    1.10    /* misc entities */
    1.11