highlight via foreground painter, using alpha channel;
authorwenzelm
Sat Jun 18 14:48:56 2011 +0200 (2011-06-18)
changeset 43435ae6b0c3e58a8
parent 43434 2fd41645813d
child 43436 13afd4634ac3
highlight via foreground painter, using alpha channel;
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 12:58:41 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 14:48:56 2011 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4    val bad_color = new Color(255, 106, 106, 100)
     1.5    val hilite_color = new Color(255, 204, 102, 100)
     1.6  
     1.7 +  val subexp_color = new Color(0xC0, 0xC0, 0xC0, 100)
     1.8 +
     1.9    val keyword1_color = get_color("#006699")
    1.10    val keyword2_color = get_color("#009966")
    1.11  
    1.12 @@ -172,7 +174,7 @@
    1.13    val subexp: Markup_Tree.Select[(Text.Range, Color)] =
    1.14    {
    1.15      case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
    1.16 -      (range, Color.black)
    1.17 +      (range, subexp_color)
    1.18    }
    1.19  
    1.20  
     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 12:58:41 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jun 18 14:48:56 2011 +0200
     2.3 @@ -121,18 +121,6 @@
     2.4                gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
     2.5              }
     2.6  
     2.7 -            // sub-expression highlighting -- potentially from other snapshot
     2.8 -            doc_view.highlight_range match {
     2.9 -              case Some((range, color)) if line_range.overlaps(range) =>
    2.10 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    2.11 -                  case None =>
    2.12 -                  case Some(r) =>
    2.13 -                    gfx.setColor(color)
    2.14 -                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    2.15 -                }
    2.16 -              case _ =>
    2.17 -            }
    2.18 -
    2.19              // squiggly underline
    2.20              for {
    2.21                Text.Info(range, Some(color)) <-
    2.22 @@ -304,6 +292,39 @@
    2.23    }
    2.24  
    2.25  
    2.26 +  /* foreground */
    2.27 +
    2.28 +  private val foreground_painter = new TextAreaExtension
    2.29 +  {
    2.30 +    override def paintScreenLineRange(gfx: Graphics2D,
    2.31 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
    2.32 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    2.33 +    {
    2.34 +      doc_view.robust_body(()) {
    2.35 +        val snapshot = painter_snapshot
    2.36 +
    2.37 +        for (i <- 0 until physical_lines.length) {
    2.38 +          if (physical_lines(i) != -1) {
    2.39 +            val line_range = doc_view.proper_line_range(start(i), end(i))
    2.40 +
    2.41 +            // highlighted range -- potentially from other snapshot
    2.42 +            doc_view.highlight_range match {
    2.43 +              case Some((range, color)) if line_range.overlaps(range) =>
    2.44 +                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    2.45 +                  case None =>
    2.46 +                  case Some(r) =>
    2.47 +                    gfx.setColor(color)
    2.48 +                    gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.49 +                }
    2.50 +              case _ =>
    2.51 +            }
    2.52 +          }
    2.53 +        }
    2.54 +      }
    2.55 +    }
    2.56 +  }
    2.57 +
    2.58 +
    2.59    /* caret -- outside of text range */
    2.60  
    2.61    private class Caret_Painter(before: Boolean) extends TextAreaExtension
    2.62 @@ -359,6 +380,7 @@
    2.63      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
    2.64      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
    2.65      painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
    2.66 +    painter.addExtension(500, foreground_painter)
    2.67      painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
    2.68      painter.removeExtension(orig_text_painter)
    2.69    }
    2.70 @@ -368,6 +390,7 @@
    2.71      val painter = text_area.getPainter
    2.72      painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
    2.73      painter.removeExtension(reset_state)
    2.74 +    painter.removeExtension(foreground_painter)
    2.75      painter.removeExtension(caret_painter)
    2.76      painter.removeExtension(after_caret_painter2)
    2.77      painter.removeExtension(before_caret_painter2)