src/Pure/General/markup.scala
changeset 29482 fe044b49e34f
parent 29417 779ff1187327
child 29488 8fc3aeece219
equal deleted inserted replaced
29481:3e8420c1124a 29482:fe044b49e34f
   115   val UNPROCESSED = "unprocessed"
   115   val UNPROCESSED = "unprocessed"
   116   val RUNNING = "running"
   116   val RUNNING = "running"
   117   val FAILED = "failed"
   117   val FAILED = "failed"
   118   val FINISHED = "finished"
   118   val FINISHED = "finished"
   119   val DISPOSED = "disposed"
   119   val DISPOSED = "disposed"
       
   120   val COMMAND_STATE = "command_state"
   120 
   121 
   121 
   122 
   122   /* messages */
   123   /* messages */
   123 
   124 
   124   val PID = "pid"
   125   val PID = "pid"