src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Aug 14 11:52:24 2010 +0200
@@ -148,8 +148,7 @@
 
 class Command(
     val id: Document.Command_ID,
-    val span: Thy_Syntax.Span,
-    val static_parent: Option[Command] = None)  // FIXME !?
+    val span: List[Token])
 {
   /* classification */