src/Pure/General/markup.scala
changeset 29488 8fc3aeece219
parent 29482 fe044b49e34f
child 29522 793766d4c1b5
equal deleted inserted replaced
29487:06f4bb9fdb85 29488:8fc3aeece219
   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 
       
   122   /* interactive documents */
       
   123 
       
   124   val EDITS = "edits"
       
   125   val EDIT = "edit"
   121 
   126 
   122 
   127 
   123   /* messages */
   128   /* messages */
   124 
   129 
   125   val PID = "pid"
   130   val PID = "pid"