src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Aug 12 15:19:11 2010 +0200
@@ -27,7 +27,7 @@
   }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
-    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
+    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
 
 
 
@@ -201,9 +201,9 @@
     accumulator ! Consume(message, forward)
   }
 
-  def assign_state(state_id: Document.State_ID): Command =
+  def assign_exec(exec_id: Document.Exec_ID): Command =
   {
-    val cmd = new Command(state_id, span, Some(this))
+    val cmd = new Command(exec_id, span, Some(this))
     accumulator !? Assign
     cmd.state = current_state
     cmd