1.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Jan 13 12:31:22 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 14 12:36:43 2012 +0100
     1.3 @@ -105,19 +105,6 @@
     1.4        Int_Property("relative-font-size", 100)).toFloat / 100
     1.5  
     1.6  
     1.7 -  /* text area ranges */
     1.8 -
     1.9 -  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.10 -
    1.11 -  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.12 -  {
    1.13 -    val p = text_area.offsetToXY(range.start)
    1.14 -    val q = text_area.offsetToXY(range.stop)
    1.15 -    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
    1.16 -    else None
    1.17 -  }
    1.18 -
    1.19 -
    1.20    /* tooltip markup */
    1.21  
    1.22    def tooltip(text: String): String =

     2.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jan 13 12:31:22 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Sat Jan 14 12:36:43 2012 +0100
     2.3 @@ -26,6 +26,19 @@
     2.4    private val text_area = doc_view.text_area
     2.5  
     2.6  
     2.7 +  /* text area ranges */
     2.8 +
     2.9 +  private class Gfx_Range(val x: Int, val y: Int, val length: Int)
    2.10 +
    2.11 +  private def gfx_range(range: Text.Range): Option[Gfx_Range] =
    2.12 +  {
    2.13 +    val p = text_area.offsetToXY(range.start)
    2.14 +    val q = text_area.offsetToXY(range.stop)
    2.15 +    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
    2.16 +    else None
    2.17 +  }
    2.18 +
    2.19 +
    2.20    /* original painters */
    2.21  
    2.22    private def pick_extension(name: String): TextAreaExtension =
    2.23 @@ -92,7 +105,7 @@
    2.24              // background color (1)
    2.25              for {
    2.26                Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
    2.27 -              r <- Isabelle.gfx_range(text_area, range)
    2.28 +              r <- gfx_range(range)
    2.29              } {
    2.30                gfx.setColor(color)
    2.31                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.32 @@ -101,7 +114,7 @@
    2.33              // background color (2)
    2.34              for {
    2.35                Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
    2.36 -              r <- Isabelle.gfx_range(text_area, range)
    2.37 +              r <- gfx_range(range)
    2.38              } {
    2.39                gfx.setColor(color)
    2.40                gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
    2.41 @@ -110,7 +123,7 @@
    2.42              // squiggly underline
    2.43              for {
    2.44                Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
    2.45 -              r <- Isabelle.gfx_range(text_area, range)
    2.46 +              r <- gfx_range(range)
    2.47              } {
    2.48                gfx.setColor(color)
    2.49                val x0 = (r.x / 2) * 2
    2.50 @@ -303,7 +316,7 @@
    2.51              // foreground color
    2.52              for {
    2.53                Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
    2.54 -              r <- Isabelle.gfx_range(text_area, range)
    2.55 +              r <- gfx_range(range)
    2.56              } {
    2.57                gfx.setColor(color)
    2.58                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
    2.59 @@ -312,7 +325,7 @@
    2.60              // highlighted range -- potentially from other snapshot
    2.61              doc_view.highlight_range match {
    2.62                case Some((range, color)) if line_range.overlaps(range) =>
    2.63 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
    2.64 +                gfx_range(line_range.restrict(range)) match {
    2.65                    case None =>
    2.66                    case Some(r) =>
    2.67                      gfx.setColor(color)