src/Pure/PIDE/markup.scala
changeset 59186 45e31a196b57
parent 59184 830bb7ddb3ab
child 59203 5f0bd5afc16d
equal deleted inserted replaced
59185:08ff767a82bf 59186:45e31a196b57
   341 
   341 
   342   /* messages */
   342   /* messages */
   343 
   343 
   344   val SERIAL = "serial"
   344   val SERIAL = "serial"
   345   val Serial = new Properties.Long(SERIAL)
   345   val Serial = new Properties.Long(SERIAL)
   346 
       
   347   val MESSAGE = "message"
       
   348 
   346 
   349   val INIT = "init"
   347   val INIT = "init"
   350   val STATUS = "status"
   348   val STATUS = "status"
   351   val REPORT = "report"
   349   val REPORT = "report"
   352   val RESULT = "result"
   350   val RESULT = "result"