--- a/src/Pure/PIDE/command.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 05 14:35:35 2010 +0200
@@ -35,7 +35,7 @@
}
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
@@ -91,7 +91,7 @@
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