src/Pure/PIDE/markup.scala
changeset 52877 9a26ec5739dd
parent 52876 78989972d5b8
child 53055 0fe8a9972eda
     1.1 --- a/src/Pure/PIDE/markup.scala	Tue Aug 06 21:08:04 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Tue Aug 06 21:34:58 2013 +0200
     1.3 @@ -245,8 +245,6 @@
     1.4    val FINISHED = "finished"
     1.5    val FAILED = "failed"
     1.6  
     1.7 -  val WAITING = "waiting"
     1.8 -
     1.9  
    1.10    /* interactive documents */
    1.11