src/Tools/jEdit/src/isabelle_rendering.scala
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46166 4beb2f41ed93
     1.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Dec 01 13:34:16 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Dec 01 14:29:14 2011 +0100
     1.3 @@ -61,9 +61,9 @@
     1.4      val state = snapshot.command_state(command)
     1.5      if (snapshot.is_outdated) Some(outdated_color)
     1.6      else
     1.7 -      Isabelle_Document.command_status(state.status) match {
     1.8 -        case Isabelle_Document.Forked(i) if i > 0 => Some(running1_color)
     1.9 -        case Isabelle_Document.Unprocessed => Some(unprocessed1_color)
    1.10 +      Protocol.command_status(state.status) match {
    1.11 +        case Protocol.Forked(i) if i > 0 => Some(running1_color)
    1.12 +        case Protocol.Unprocessed => Some(unprocessed1_color)
    1.13          case _ => None
    1.14        }
    1.15    }
    1.16 @@ -73,13 +73,13 @@
    1.17      val state = snapshot.command_state(command)
    1.18      if (snapshot.is_outdated) None
    1.19      else
    1.20 -      Isabelle_Document.command_status(state.status) match {
    1.21 -        case Isabelle_Document.Forked(i) => if (i > 0) Some(running_color) else None
    1.22 -        case Isabelle_Document.Unprocessed => Some(unprocessed_color)
    1.23 -        case Isabelle_Document.Failed => Some(error_color)
    1.24 -        case Isabelle_Document.Finished =>
    1.25 -          if (state.results.exists(r => Isabelle_Document.is_error(r._2))) Some(error_color)
    1.26 -          else if (state.results.exists(r => Isabelle_Document.is_warning(r._2))) Some(warning_color)
    1.27 +      Protocol.command_status(state.status) match {
    1.28 +        case Protocol.Forked(i) => if (i > 0) Some(running_color) else None
    1.29 +        case Protocol.Unprocessed => Some(unprocessed_color)
    1.30 +        case Protocol.Failed => Some(error_color)
    1.31 +        case Protocol.Finished =>
    1.32 +          if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
    1.33 +          else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
    1.34            else None
    1.35        }
    1.36    }