clarified painting of invisible caret, e.g. focus change due to popup;
authorwenzelm
Mon Feb 24 12:51:55 2014 +0100 (2014-02-24 ago)
changeset 55713734ac5709fbe
parent 55712 e757e8c8d8ea
child 55714 ed1b789d0b21
clarified painting of invisible caret, e.g. focus change due to popup;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Mon Feb 24 12:23:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Mon Feb 24 12:51:55 2014 +0100
     1.3 @@ -85,6 +85,7 @@
     1.4  option keyword1_color : string = "006699FF"
     1.5  option keyword2_color : string = "009966FF"
     1.6  option keyword3_color : string = "0099FFFF"
     1.7 +option caret_invisible_color : string = "99999980"
     1.8  
     1.9  option tfree_color : string = "A020F0FF"
    1.10  option tvar_color : string = "A020F0FF"
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:23:35 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:51:55 2014 +0100
     2.3 @@ -260,6 +260,7 @@
     2.4    val keyword1_color = color_value("keyword1_color")
     2.5    val keyword2_color = color_value("keyword2_color")
     2.6    val keyword3_color = color_value("keyword3_color")
     2.7 +  val caret_invisible_color = color_value("caret_invisible_color")
     2.8  
     2.9    val tfree_color = color_value("tfree_color")
    2.10    val tvar_color = color_value("tvar_color")
     3.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 12:23:35 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Feb 24 12:51:55 2014 +0100
     3.3 @@ -222,16 +222,25 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* text background */
     3.8 +  /* caret */
     3.9  
    3.10    private def get_caret_range(stretch: Boolean): Text.Range =
    3.11 -    if (caret_visible && text_area.isCaretVisible) {
    3.12 +    if (caret_visible) {
    3.13        val caret = text_area.getCaretPosition
    3.14        if (stretch) JEdit_Lib.stretch_point_range(buffer, caret)
    3.15        else JEdit_Lib.point_range(buffer, caret)
    3.16      }
    3.17      else Text.Range(-1)
    3.18  
    3.19 +  private def get_caret_color(rendering: Rendering): Color =
    3.20 +  {
    3.21 +    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
    3.22 +    else rendering.caret_invisible_color
    3.23 +  }
    3.24 +
    3.25 +
    3.26 +  /* text background */
    3.27 +
    3.28    private val background_painter = new TextAreaExtension
    3.29    {
    3.30      override def paintScreenLineRange(gfx: Graphics2D,
    3.31 @@ -360,7 +369,7 @@
    3.32  
    3.33                val astr = new AttributedString(s2)
    3.34                astr.addAttribute(TextAttribute.FONT, chunk_font)
    3.35 -              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
    3.36 +              astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering))
    3.37                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
    3.38                gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
    3.39  
    3.40 @@ -446,7 +455,6 @@
    3.41        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.42      {
    3.43        robust_rendering { rendering =>
    3.44 -        val painter = text_area.getPainter
    3.45          val caret_range = get_caret_range(true)
    3.46  
    3.47          for (i <- 0 until physical_lines.length) {
    3.48 @@ -486,7 +494,7 @@
    3.49              if (!hyperlink_area.is_active) {
    3.50                def paint_completion(range: Text.Range) {
    3.51                  for (r <- JEdit_Lib.gfx_range(text_area, range)) {
    3.52 -                  gfx.setColor(painter.getCaretColor)
    3.53 +                  gfx.setColor(get_caret_color(rendering))
    3.54                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    3.55                  }
    3.56                }
    3.57 @@ -531,8 +539,8 @@
    3.58      override def paintValidLine(gfx: Graphics2D,
    3.59        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
    3.60      {
    3.61 -      robust_rendering { _ =>
    3.62 -        if (caret_visible && text_area.isCaretVisible) {
    3.63 +      robust_rendering { rendering =>
    3.64 +        if (caret_visible) {
    3.65            val caret = text_area.getCaretPosition
    3.66            if (start <= caret && caret == end - 1) {
    3.67              val painter = text_area.getPainter
    3.68 @@ -541,7 +549,7 @@
    3.69  
    3.70              val offset = caret - text_area.getLineStartOffset(physical_line)
    3.71              val x = text_area.offsetToXY(physical_line, offset).x
    3.72 -            gfx.setColor(painter.getCaretColor)
    3.73 +            gfx.setColor(get_caret_color(rendering))
    3.74              gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
    3.75            }
    3.76          }