--- a/src/Pure/PIDE/command.scala Thu Aug 12 13:43:55 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 12 13:49:08 2010 +0200
@@ -13,9 +13,6 @@
import scala.collection.mutable
-case class Command_Set(set: Set[Command])
-
-
object Command
{
object Status extends Enumeration