unused;
authorwenzelm
Tue Dec 23 21:14:44 2014 +0100 (2014-12-23)
changeset 5918645e31a196b57
parent 59185 08ff767a82bf
child 59187 5a783837b50b
unused;
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Dec 23 21:04:53 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Dec 23 21:14:44 2014 +0100
     1.3 @@ -344,8 +344,6 @@
     1.4    val SERIAL = "serial"
     1.5    val Serial = new Properties.Long(SERIAL)
     1.6  
     1.7 -  val MESSAGE = "message"
     1.8 -
     1.9    val INIT = "init"
    1.10    val STATUS = "status"
    1.11    val REPORT = "report"