src/Pure/PIDE/markup.scala
changeset 68884 9b97d0b20d95
parent 68871 f5c76072db55
child 68997 4278947ba336
equal deleted inserted replaced
68883:3653b3ad729e 68884:9b97d0b20d95
   424   val RUNNING = "running"
   424   val RUNNING = "running"
   425   val FINISHED = "finished"
   425   val FINISHED = "finished"
   426   val FAILED = "failed"
   426   val FAILED = "failed"
   427   val CANCELED = "canceled"
   427   val CANCELED = "canceled"
   428   val INITIALIZED = "initialized"
   428   val INITIALIZED = "initialized"
       
   429   val FINALIZED = "finalized"
   429   val CONSOLIDATED = "consolidated"
   430   val CONSOLIDATED = "consolidated"
   430 
   431 
   431 
   432 
   432   /* interactive documents */
   433   /* interactive documents */
   433 
   434