src/Pure/PIDE/command.scala

   case class RefInfo(file: Option[String], line: Option[Int],
     command_id: Option[String], offset: Option[Int])
 }
 
 class Command(
-    val id: Isar_Document.Command_ID,
+    val id: Document.Command_ID,
     val span: Thy_Syntax.Span,
     val static_parent: Option[Command] = None)
   extends Session.Entity
 {
   /* classification */

   def consume(message: XML.Tree, forward: Command => Unit)
   {
     accumulator ! Consume(message, forward)
   }
 
-  def assign_state(state_id: Isar_Document.State_ID): Command =
+  def assign_state(state_id: Document.State_ID): Command =
   {
     val cmd = new Command(state_id, span, Some(this))
     accumulator !? Assign
     cmd.state = current_state
     cmd