# HG changeset patch
# User wenzelm
# Date 1348172730 -7200
# Node ID 8f3a3adadd5adc46c820089194528689473c03ca
# Parent  e7ff10e1a15507d3e5e3775050aa340a37cebfa0
tuned painter;

diff -r e7ff10e1a155 -r 8f3a3adadd5a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Sep 20 21:57:37 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Sep 20 22:25:30 2012 +0200
@@ -150,8 +150,11 @@
   override def isCaretVisible: Boolean = false
 
   getPainter.setStructureHighlightEnabled(false)
+  getPainter.setLineHighlightEnabled(false)
+
   getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
   getBuffer.setReadOnly(true)
+
   rich_text_area.activate()
 }
 
diff -r e7ff10e1a155 -r 8f3a3adadd5a src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 21:57:37 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Sep 20 22:25:30 2012 +0200
@@ -202,8 +202,8 @@
             for { (color, separator) <- rendering.line_background(line_range) }
             {
               gfx.setColor(color)
-              val tweak = if (separator) (2 min (line_height / 2)) else 0
-              gfx.fillRect(0, y + i * line_height - tweak, text_area.getWidth, line_height - tweak)
+              val sep = if (separator) (2 min (line_height / 2)) else 0
+              gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
             }
 
             // background color (1)