# HG changeset patch
# User wenzelm
# Date 1326541003 -3600
# Node ID df1369a42393437e87e6ddc0fd0704fa83fe8225
# Parent  d43ddad41d81435b84d31a00a883734639f90f11
tuned signature;

diff -r d43ddad41d81 -r df1369a42393 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Jan 13 12:31:22 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 14 12:36:43 2012 +0100
@@ -105,19 +105,6 @@
       Int_Property("relative-font-size", 100)).toFloat / 100
 
 
-  /* text area ranges */
-
-  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
-
-  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
-  {
-    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))
-    else None
-  }
-
-
   /* tooltip markup */
 
   def tooltip(text: String): String =
diff -r d43ddad41d81 -r df1369a42393 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jan 13 12:31:22 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jan 14 12:36:43 2012 +0100
@@ -26,6 +26,19 @@
   private val text_area = doc_view.text_area
 
 
+  /* text area ranges */
+
+  private class Gfx_Range(val x: Int, val y: Int, val length: Int)
+
+  private def gfx_range(range: Text.Range): Option[Gfx_Range] =
+  {
+    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))
+    else None
+  }
+
+
   /* original painters */
 
   private def pick_extension(name: String): TextAreaExtension =
@@ -92,7 +105,7 @@
             // background color (1)
             for {
               Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
-              r <- Isabelle.gfx_range(text_area, range)
+              r <- gfx_range(range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
@@ -101,7 +114,7 @@
             // background color (2)
             for {
               Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
-              r <- Isabelle.gfx_range(text_area, range)
+              r <- gfx_range(range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
@@ -110,7 +123,7 @@
             // squiggly underline
             for {
               Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
-              r <- Isabelle.gfx_range(text_area, range)
+              r <- gfx_range(range)
             } {
               gfx.setColor(color)
               val x0 = (r.x / 2) * 2
@@ -303,7 +316,7 @@
             // foreground color
             for {
               Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
-              r <- Isabelle.gfx_range(text_area, range)
+              r <- gfx_range(range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
@@ -312,7 +325,7 @@
             // highlighted range -- potentially from other snapshot
             doc_view.highlight_range match {
               case Some((range, color)) if line_range.overlaps(range) =>
-                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+                gfx_range(line_range.restrict(range)) match {
                   case None =>
                   case Some(r) =>
                     gfx.setColor(color)