1.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:58:41 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 14:48:56 2011 +0200
     1.3 @@ -121,18 +121,6 @@
     1.4                gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
     1.5              }
     1.6  
     1.7 -            // sub-expression highlighting -- potentially from other snapshot
     1.8 -            doc_view.highlight_range match {
     1.9 -              case Some((range, color)) if line_range.overlaps(range) =>
    1.10 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    1.11 -                  case None =>
    1.12 -                  case Some(r) =>
    1.13 -                    gfx.setColor(color)
    1.14 -                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    1.15 -                }
    1.16 -              case _ =>
    1.17 -            }
    1.18 -
    1.19              // squiggly underline
    1.20              for {
    1.21                Text.Info(range, Some(color)) <-
    1.22 @@ -304,6 +292,39 @@
    1.23    }
    1.24  
    1.25  
    1.26 +  /* foreground */
    1.27 +
    1.28 +  private val foreground_painter = new TextAreaExtension
    1.29 +  {
    1.30 +    override def paintScreenLineRange(gfx: Graphics2D,
    1.31 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.32 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.33 +    {
    1.34 +      doc_view.robust_body(()) {
    1.35 +        val snapshot = painter_snapshot
    1.36 +
    1.37 +        for (i <- 0 until physical_lines.length) {
    1.38 +          if (physical_lines(i) != -1) {
    1.39 +            val line_range = doc_view.proper_line_range(start(i), end(i))
    1.40 +
    1.41 +            // highlighted range -- potentially from other snapshot
    1.42 +            doc_view.highlight_range match {
    1.43 +              case Some((range, color)) if line_range.overlaps(range) =>
    1.44 +                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    1.45 +                  case None =>
    1.46 +                  case Some(r) =>
    1.47 +                    gfx.setColor(color)
    1.48 +                    gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    1.49 +                }
    1.50 +              case _ =>
    1.51 +            }
    1.52 +          }
    1.53 +        }
    1.54 +      }
    1.55 +    }
    1.56 +  }
    1.57 +
    1.58 +
    1.59    /* caret -- outside of text range */
    1.60  
    1.61    private class Caret_Painter(before: Boolean) extends TextAreaExtension
    1.62 @@ -359,6 +380,7 @@
    1.63      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
    1.64      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
    1.65      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
    1.66 +    painter.addExtension(500, foreground_painter)
    1.67      painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
    1.68      painter.removeExtension(orig_text_painter)
    1.69    }
    1.70 @@ -368,6 +390,7 @@
    1.71      val painter = text_area.getPainter
    1.72      painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
    1.73      painter.removeExtension(reset_state)
    1.74 +    painter.removeExtension(foreground_painter)
    1.75      painter.removeExtension(caret_painter)
    1.76      painter.removeExtension(after_caret_painter2)
    1.77      painter.removeExtension(before_caret_painter2)