src/Tools/jEdit/src/rich_text_area.scala
changeset 62986 9d2fae6b31cc
parent 62812 ce22e5c3d4ce
child 62988 224e8d8a4fb8
     1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 14 20:47:44 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 14 22:55:53 2016 +0200
     1.3 @@ -280,6 +280,13 @@
     1.4        robust_rendering { rendering =>
     1.5          val fm = text_area.getPainter.getFontMetrics
     1.6  
     1.7 +        val focus =
     1.8 +          JEdit_Lib.visible_range(text_area) match {
     1.9 +            case Some(visible_range) if caret_enabled =>
    1.10 +              rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
    1.11 +            case _ => Set.empty[Long]
    1.12 +          }
    1.13 +
    1.14          for (i <- 0 until physical_lines.length) {
    1.15            if (physical_lines(i) != -1) {
    1.16              val line_range = Text.Range(start(i), end(i) min buffer.getLength)
    1.17 @@ -294,7 +301,7 @@
    1.18  
    1.19              // background color
    1.20              for {
    1.21 -              Text.Info(range, color) <- rendering.background(line_range)
    1.22 +              Text.Info(range, color) <- rendering.background(line_range, focus)
    1.23                r <- JEdit_Lib.gfx_range(text_area, range)
    1.24              } {
    1.25                gfx.setColor(color)