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

     2.1 --- a/src/Pure/PIDE/document.scala	Thu May 20 10:31:20 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu May 20 10:43:46 2010 +0200
     2.3 @@ -175,9 +175,12 @@
     2.4      System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
     2.5    }
     2.6  
     2.7 -  def current_state(cmd: Command): Option[State] =
     2.8 +  def current_state(cmd: Command): State =
     2.9    {
    2.10      require(assignment.is_finished)
    2.11 -    (assignment.join).get(cmd).map(_.current_state)
    2.12 +    (assignment.join).get(cmd) match {
    2.13 +      case Some(cmd_state) => cmd_state.current_state
    2.14 +      case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
    2.15 +    }
    2.16    }
    2.17  }

     3.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 20 10:31:20 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 20 10:43:46 2010 +0200
     3.3 @@ -25,11 +25,11 @@
     3.4  {
     3.5    def choose_color(command: Command, doc: Document): Color =
     3.6    {
     3.7 -    doc.current_state(command).map(_.status) match {
     3.8 -      case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
     3.9 -      case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
    3.10 -      case Some(Command.Status.FAILED) => new Color(255, 193, 193)
    3.11 -      case _ => Color.red
    3.12 +    doc.current_state(command).status match {
    3.13 +      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    3.14 +      case Command.Status.FINISHED => new Color(234, 248, 255)
    3.15 +      case Command.Status.FAILED => new Color(255, 193, 193)
    3.16 +      case Command.Status.UNDEFINED => Color.red
    3.17      }
    3.18    }
    3.19  
    3.20 @@ -146,7 +146,7 @@
    3.21        val offset = model.from_current(document, text_area.xyToOffset(x, y))
    3.22        document.command_at(offset) match {
    3.23          case Some((command, command_start)) =>
    3.24 -          document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
    3.25 +          document.current_state(command).type_at(offset - command_start) getOrElse null
    3.26          case None => null
    3.27        }
    3.28      }

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

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

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

     7.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 10:31:20 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 10:43:46 2010 +0200
     7.3 @@ -46,7 +46,7 @@
     7.4            val document = model.recent_document
     7.5            document.command_at(view.getTextArea.getCaretPosition) match {
     7.6              case Some((cmd, _)) =>
     7.7 -              output_actor ! Render(document.current_state(cmd).map(_.results) getOrElse Nil)
     7.8 +              output_actor ! Render(document.current_state(cmd).results)
     7.9              case None =>
    7.10            }
    7.11          case None =>
    7.12 @@ -76,9 +76,7 @@
    7.13              if (follow.selected) Document_Model(view.getBuffer) else None
    7.14            } match {
    7.15              case None =>
    7.16 -            case Some(model) =>
    7.17 -              val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
    7.18 -              html_panel.render(body)
    7.19 +            case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
    7.20            }
    7.21  
    7.22          case bad => System.err.println("output_actor: ignoring bad message " + bad)