# HG changeset patch
# User wenzelm
# Date 1277580395 -7200
# Node ID d57d0f581d381a456a30f50d1ec64984e6ea0ba1
# Parent  6c7399bc0d10577829e8b4a5144530b3ddf8541c
simplified text_area_painter, with more precise treatment of visible line end;

diff -r 6c7399bc0d10 -r d57d0f581d38 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jun 25 14:05:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Jun 26 21:26:35 2010 +0200
@@ -56,6 +56,19 @@
 
 class Document_Model(val session: Session, val buffer: Buffer)
 {
+  /* visible line end */
+
+  // simplify slightly odd result of TextArea.getLineEndOffset
+  // NB: jEdit already normalizes \r\n and \r to \n
+  def visible_line_end(start: Int, end: Int): Int =
+  {
+    val end1 = end - 1
+    if (start <= end1 && end1 < buffer.getLength &&
+        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
+    else end
+  }
+
+
   /* history */
 
   private val document_0 = session.begin_document(buffer.getName)
diff -r 6c7399bc0d10 -r d57d0f581d38 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Jun 25 14:05:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Jun 26 21:26:35 2010 +0200
@@ -129,16 +129,20 @@
       val document = model.recent_document()
       def from_current(pos: Int) = model.from_current(document, pos)
       def to_current(pos: Int) = model.to_current(document, pos)
-      val metrics = text_area.getPainter.getFontMetrics
+
+      val line_end = model.visible_line_end(start, end)
+      val line_height = text_area.getPainter.getFontMetrics.getHeight
+
       val saved_color = gfx.getColor
       try {
         for ((command, command_start) <-
-          document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
+          document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
         {
-          val begin = start max to_current(command_start)
-          val finish = (end - 1) min to_current(command_start + command.length)
-          encolor(gfx, y, metrics.getHeight, begin, finish,
-            Document_View.choose_color(document, command), true)
+          val p = text_area.offsetToXY(start max to_current(command_start))
+          val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+          assert(p.y == q.y)
+          gfx.setColor(Document_View.choose_color(document, command))
+          gfx.fillRect(p.x, y, q.x - p.x, line_height)
         }
       }
       finally { gfx.setColor(saved_color) }
@@ -205,26 +209,6 @@
     text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
       text_area.getLastPhysicalLine)
 
-  private def encolor(gfx: Graphics2D,
-    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
-  {
-    val start = text_area.offsetToXY(begin)
-    val stop =
-      if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
-      else {
-        val p = text_area.offsetToXY(finish - 1)
-        val metrics = text_area.getPainter.getFontMetrics
-        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
-        p
-      }
-
-    if (start != null && stop != null) {
-      gfx.setColor(color)
-      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
-      else gfx.drawRect(start.x, y, stop.x - start.x, height)
-    }
-  }
-
 
   /* overview of command status left of scrollbar */