1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jan 11 18:28:31 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jan 11 20:51:58 2010 +0100
     1.3 @@ -25,10 +25,10 @@
     1.4  {
     1.5    def choose_color(command: Command, doc: Document): Color =
     1.6    {
     1.7 -    doc.current_state(command).status match {
     1.8 -      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
     1.9 -      case Command.Status.FINISHED => new Color(234, 248, 255)
    1.10 -      case Command.Status.FAILED => new Color(255, 193, 193)
    1.11 +    doc.current_state(command).map(_.status) match {
    1.12 +      case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
    1.13 +      case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
    1.14 +      case Some(Command.Status.FAILED) => new Color(255, 193, 193)
    1.15        case _ => Color.red
    1.16      }
    1.17    }
    1.18 @@ -146,7 +146,7 @@
    1.19        val offset = model.from_current(document, text_area.xyToOffset(x, y))
    1.20        document.command_at(offset) match {
    1.21          case Some((command, command_start)) =>
    1.22 -          document.current_state(command).type_at(offset - command_start).getOrElse(null)
    1.23 +          document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
    1.24          case None => null
    1.25        }
    1.26      }