1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 02 23:26:21 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 02 23:27:41 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
     1.6  import org.gjt.sp.jedit.buffer.JEditBuffer
     1.7 -import org.gjt.sp.jedit.textarea.JEditTextArea
     1.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     1.9  import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
    1.10  import org.gjt.sp.jedit.gui.DockableWindowManager
    1.11  
    1.12 @@ -74,6 +74,19 @@
    1.13        Int_Property("relative-font-size", 100)).toFloat / 100
    1.14  
    1.15  
    1.16 +  /* text area ranges */
    1.17 +
    1.18 +  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    1.19 +
    1.20 +  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.21 +  {
    1.22 +    val p = text_area.offsetToXY(range.start)
    1.23 +    val q = text_area.offsetToXY(range.stop)
    1.24 +    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
    1.25 +    else None
    1.26 +  }
    1.27 +
    1.28 +
    1.29    /* tooltip markup */
    1.30  
    1.31    def tooltip(text: String): String =