# HG changeset patch
# User wenzelm
# Date 1283462861 -7200
# Node ID a0d7e9b580ec1d8df51d4cd518d3c259f3a9d239
# Parent  470fd769ae532c57054bf802ca37186b8ea61b5d
added gfx_range convenience;

diff -r 470fd769ae53 -r a0d7e9b580ec src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 02 23:26:21 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 02 23:27:41 2010 +0200
@@ -17,7 +17,7 @@
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
@@ -74,6 +74,19 @@
       Int_Property("relative-font-size", 100)).toFloat / 100
 
 
+  /* text area ranges */
+
+  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 =