ignore empty gfx_range;
tuned;

--- a/src/Tools/jEdit/src/document_view.scala	Sat Jan 14 12:36:43 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Jan 14 13:11:32 2012 +0100
@@ -210,18 +210,8 @@
 
   /* subexpression highlighting */
 
-  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
-    : Option[(Text.Range, Color)] =
-  {
-    val offset = text_area.xyToOffset(x, y)
-    Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
-  }
-
-  @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
-  def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
-
-
-  /* CONTROL-mouse management */
+  @volatile private var _highlight_range: Option[Text.Info[Color]] = None
+  def highlight_range(): Option[Text.Info[Color]] = _highlight_range
 
   private var control: Boolean = false
 
@@ -255,9 +245,14 @@
 
           if (control) init_popup(snapshot, x, y)
 
-          _highlight_range map { case (range, _) => invalidate_range(range) }
-          _highlight_range = if (control) subexp_range(snapshot, x, y) else None
-          _highlight_range map { case (range, _) => invalidate_range(range) }
+          for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
+          _highlight_range =
+            if (control) {
+              val offset = text_area.xyToOffset(x, y)
+              Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
+            }
+            else None
+          for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
         }
     }
   }

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 12:36:43 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Jan 14 13:11:32 2012 +0100
@@ -245,16 +245,13 @@
       Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
       Isabelle_Markup.DOC_SOURCE)
 
-  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[(Text.Range, Color)] =
+  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
   {
     snapshot.select_markup(range, Some(subexp_include),
         {
           case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-            (range, subexp_color)
-        }) match {
-      case Text.Info(_, (range, color)) #:: _ => Some((snapshot.convert(range), color))
-      case _ => None
-    }
+            Text.Info(snapshot.convert(range), subexp_color)
+        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   }
 
 

--- 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)
             }
           }
         }