src/Tools/jEdit/src/rich_text_area.scala
changeset 65176 908d8be90533
parent 65124 759c64c39a6f
child 65213 51c0f094dc02
     1.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 18:12:52 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 21:47:48 2017 +0100
     1.3 @@ -309,7 +309,8 @@
     1.4  
     1.5              // background color
     1.6              for {
     1.7 -              Text.Info(range, c) <- rendering.background(line_range, caret_focus)
     1.8 +              Text.Info(range, c) <-
     1.9 +                rendering.background(Rendering.background_elements, line_range, caret_focus)
    1.10                r <- JEdit_Lib.gfx_range(text_area, range)
    1.11              } {
    1.12                gfx.setColor(rendering.color(c))