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