src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu May 20 10:43:46 2010 +0200
@@ -175,9 +175,12 @@
     System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
   }
 
-  def current_state(cmd: Command): Option[State] =
+  def current_state(cmd: Command): State =
   {
     require(assignment.is_finished)
-    (assignment.join).get(cmd).map(_.current_state)
+    (assignment.join).get(cmd) match {
+      case Some(cmd_state) => cmd_state.current_state
+      case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
+    }
   }
 }