src/Tools/jEdit/src/text_area_painter.scala

--- a/src/Tools/jEdit/src/text_area_painter.scala	Sat Jan 14 12:36:43 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jan 14 13:11:32 2012 +0100
@@ -34,7 +34,8 @@
   {
     val p = text_area.offsetToXY(range.start)
     val q = text_area.offsetToXY(range.stop)
-    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
+    if (p != null && q != null && p.x < q.x && p.y == q.y)
+      Some(new Gfx_Range(p.x, p.y, q.x - p.x))
     else None
   }
 
@@ -323,15 +324,13 @@
             }
 
             // highlighted range -- potentially from other snapshot
-            doc_view.highlight_range match {
-              case Some((range, color)) if line_range.overlaps(range) =>
-                gfx_range(line_range.restrict(range)) match {
-                  case None =>
-                  case Some(r) =>
-                    gfx.setColor(color)
-                    gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
-                }
-              case _ =>
+            for {
+              info <- doc_view.highlight_range()
+              Text.Info(range, color) <- info.try_restrict(line_range)
+              r <- gfx_range(range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
           }
         }