explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];

--- a/src/Pure/PIDE/command.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu May 20 10:43:46 2010 +0200
@@ -20,6 +20,7 @@
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
     val FAILED = Value("FAILED")
+    val UNDEFINED = Value("UNDEFINED")
   }
 
   case class HighlightInfo(highlight: String) { override def toString = highlight }

--- 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)
+    }
   }
 }

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 20 10:43:46 2010 +0200
@@ -25,11 +25,11 @@
 {
   def choose_color(command: Command, doc: Document): Color =
   {
-    doc.current_state(command).map(_.status) match {
-      case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
-      case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
-      case Some(Command.Status.FAILED) => new Color(255, 193, 193)
-      case _ => Color.red
+    doc.current_state(command).status match {
+      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+      case Command.Status.FINISHED => new Color(234, 248, 255)
+      case Command.Status.FAILED => new Color(255, 193, 193)
+      case Command.Status.UNDEFINED => Color.red
     }
   }
 
@@ -146,7 +146,7 @@
       val offset = model.from_current(document, text_area.xyToOffset(x, y))
       document.command_at(offset) match {
         case Some((command, command_start)) =>
-          document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
+          document.current_state(command).type_at(offset - command_start) getOrElse null
         case None => null
       }
     }

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu May 20 10:43:46 2010 +0200
@@ -46,7 +46,7 @@
         val offset = model.from_current(document, original_offset)
         document.command_at(offset) match {
           case Some((command, command_start)) =>
-            document.current_state(command).get.ref_at(offset - command_start) match {
+            document.current_state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
                 val begin = model.to_current(document, command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu May 20 10:43:46 2010 +0200
@@ -130,7 +130,7 @@
     val root = data.root
     val document = model.recent_document()
     for ((command, command_start) <- document.command_range(0) if !stopped) {
-      root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
+      root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
           {
             val content = command.source(node.start, node.stop).replace('\n', ' ')
             val id = command.id

--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu May 20 10:43:46 2010 +0200
@@ -116,7 +116,7 @@
     var next_x = start
     for {
       (command, command_start) <- document.command_range(from(start), from(stop))
-      markup <- document.current_state(command).get.highlight.flatten
+      markup <- document.current_state(command).highlight.flatten
       val abs_start = to(command_start + markup.start)
       val abs_stop = to(command_start + markup.stop)
       if (abs_stop > start)

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 10:43:46 2010 +0200
@@ -46,7 +46,7 @@
           val document = model.recent_document
           document.command_at(view.getTextArea.getCaretPosition) match {
             case Some((cmd, _)) =>
-              output_actor ! Render(document.current_state(cmd).map(_.results) getOrElse Nil)
+              output_actor ! Render(document.current_state(cmd).results)
             case None =>
           }
         case None =>
@@ -76,9 +76,7 @@
             if (follow.selected) Document_Model(view.getBuffer) else None
           } match {
             case None =>
-            case Some(model) =>
-              val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
-              html_panel.render(body)
+            case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
           }
 
         case bad => System.err.println("output_actor: ignoring bad message " + bad)