Document_View: less aggressive background coloring, departing from classic PG highlighting;
authorwenzelm
Tue Sep 07 14:53:05 2010 +0200 (2010-09-07)
changeset 3916918cdf2833371
parent 39168 e3ac771235f7
child 39170 04ad0fed81f5
Document_View: less aggressive background coloring, departing from classic PG highlighting;
tuned colors;
src/Tools/jEdit/src/jedit/document_view.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 14:08:21 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 14:53:05 2010 +0200
     1.3 @@ -27,30 +27,49 @@
     1.4  {
     1.5    /* physical rendering */
     1.6  
     1.7 -  def status_color(snapshot: Document.Snapshot, command: Command): Color =
     1.8 +  val outdated_color = new Color(240, 240, 240)
     1.9 +  val unfinished_color = new Color(255, 228, 225)
    1.10 +
    1.11 +  val regular_color = new Color(192, 192, 192)
    1.12 +  val warning_color = new Color(255, 165, 0)
    1.13 +  val error_color = new Color(255, 106, 106)
    1.14 +
    1.15 +  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    1.16    {
    1.17      val state = snapshot.state(command)
    1.18 -    if (snapshot.is_outdated) new Color(240, 240, 240)
    1.19 +    if (snapshot.is_outdated) Some(outdated_color)
    1.20      else
    1.21        Isar_Document.command_status(state.status) match {
    1.22 -        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
    1.23 -        case Isar_Document.Finished => new Color(234, 248, 255)
    1.24 -        case Isar_Document.Failed => new Color(255, 193, 193)
    1.25 -        case Isar_Document.Unprocessed => new Color(255, 228, 225)
    1.26 -        case _ => Color.red
    1.27 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    1.28 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    1.29 +        case _ => None
    1.30        }
    1.31    }
    1.32  
    1.33 +  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    1.34 +  {
    1.35 +    val state = snapshot.state(command)
    1.36 +    if (snapshot.is_outdated) None
    1.37 +    else
    1.38 +      Isar_Document.command_status(state.status) match {
    1.39 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    1.40 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    1.41 +        case Isar_Document.Failed => Some(error_color)
    1.42 +        case _ => None
    1.43 +      }
    1.44 +  }
    1.45 +
    1.46 +
    1.47    val message_markup: PartialFunction[Text.Info[Any], Color] =
    1.48    {
    1.49 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(192, 192, 192)
    1.50 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
    1.51 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
    1.52 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    1.53 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    1.54 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    1.55    }
    1.56  
    1.57    val box_markup: PartialFunction[Text.Info[Any], Color] =
    1.58    {
    1.59 -    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => new Color(192, 192, 192)
    1.60 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
    1.61    }
    1.62  
    1.63  
    1.64 @@ -233,8 +252,9 @@
    1.65                  (command, command_start) <- cmds if !command.is_ignored
    1.66                  val range = line_range.restrict(snapshot.convert(command.range + command_start))
    1.67                  r <- Isabelle.gfx_range(text_area, range)
    1.68 +                color <- Document_View.status_color(snapshot, command)
    1.69                } {
    1.70 -                gfx.setColor(Document_View.status_color(snapshot, command))
    1.71 +                gfx.setColor(color)
    1.72                  gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.73                }
    1.74  
    1.75 @@ -360,12 +380,16 @@
    1.76          val snapshot = model.snapshot()
    1.77          val saved_color = gfx.getColor  // FIXME needed!?
    1.78          try {
    1.79 -          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
    1.80 +          for {
    1.81 +            (command, start) <- snapshot.node.command_starts
    1.82 +            if !command.is_ignored
    1.83              val line1 = buffer.getLineOfOffset(snapshot.convert(start))
    1.84              val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    1.85              val y = line_to_y(line1)
    1.86              val height = HEIGHT * (line2 - line1)
    1.87 -            gfx.setColor(Document_View.status_color(snapshot, command))
    1.88 +            color <- Document_View.overview_color(snapshot, command)
    1.89 +          } {
    1.90 +            gfx.setColor(color)
    1.91              gfx.fillRect(0, y, getWidth - 1, height)
    1.92            }
    1.93          }