src/Tools/jEdit/src/plugin.scala
changeset 46204 df1369a42393
parent 46117 edd50ec8d471
child 46740 852baa599351
     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 =