1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Sep 02 23:27:41 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Sep 02 23:37:14 2010 +0200
     1.3 @@ -24,7 +24,9 @@
     1.4  
     1.5  object Document_View
     1.6  {
     1.7 -  def choose_color(snapshot: Document.Snapshot, command: Command): Color =
     1.8 +  /* physical rendering */
     1.9 +
    1.10 +  def status_color(snapshot: Document.Snapshot, command: Command): Color =
    1.11    {
    1.12      val state = snapshot.state(command)
    1.13      if (snapshot.is_outdated) new Color(240, 240, 240)
    1.14 @@ -38,6 +40,13 @@
    1.15        }
    1.16    }
    1.17  
    1.18 +  val message_markup: PartialFunction[Text.Info[Any], Color] =
    1.19 +  {
    1.20 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
    1.21 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
    1.22 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
    1.23 +  }
    1.24 +
    1.25  
    1.26    /* document view of text area */
    1.27  
    1.28 @@ -163,18 +172,36 @@
    1.29        Isabelle.swing_buffer_lock(model.buffer) {
    1.30          val snapshot = model.snapshot()
    1.31          val saved_color = gfx.getColor
    1.32 +        val ascent = text_area.getPainter.getFontMetrics.getAscent
    1.33          try {
    1.34            for (i <- 0 until physical_lines.length) {
    1.35              if (physical_lines(i) != -1) {
    1.36                val line_range = proper_line_range(start(i), end(i))
    1.37 +
    1.38 +              // background color
    1.39                val cmds = snapshot.node.command_range(snapshot.revert(line_range))
    1.40 -              for ((command, command_start) <- cmds if !command.is_ignored) {
    1.41 +              for {
    1.42 +                (command, command_start) <- cmds if !command.is_ignored
    1.43                  val range = line_range.restrict(snapshot.convert(command.range + command_start))
    1.44 -                val p = text_area.offsetToXY(range.start)
    1.45 -                val q = text_area.offsetToXY(range.stop)
    1.46 -                if (p != null && q != null) {
    1.47 -                  gfx.setColor(Document_View.choose_color(snapshot, command))
    1.48 -                  gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
    1.49 +                r <- Isabelle.gfx_range(text_area, range)
    1.50 +              } {
    1.51 +                gfx.setColor(Document_View.status_color(snapshot, command))
    1.52 +                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.53 +              }
    1.54 +
    1.55 +              // squiggly underline
    1.56 +              for {
    1.57 +                Text.Info(range, color) <-
    1.58 +                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
    1.59 +                if color != null
    1.60 +                r <- Isabelle.gfx_range(text_area, range)
    1.61 +              } {
    1.62 +                gfx.setColor(color)
    1.63 +                val x0 = (r.x / 2) * 2
    1.64 +                val y0 = r.y + ascent + 1
    1.65 +                for (x1 <- Range(x0, x0 + r.length, 2)) {
    1.66 +                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
    1.67 +                  gfx.drawLine(x1, y1, x1 + 1, y1)
    1.68                  }
    1.69                }
    1.70              }
    1.71 @@ -266,7 +293,7 @@
    1.72              val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
    1.73              val y = line_to_y(line1)
    1.74              val height = HEIGHT * (line2 - line1)
    1.75 -            gfx.setColor(Document_View.choose_color(snapshot, command))
    1.76 +            gfx.setColor(Document_View.status_color(snapshot, command))
    1.77              gfx.fillRect(0, y, getWidth - 1, height)
    1.78            }
    1.79          }