src/Tools/jEdit/src/jedit_lib.scala
changeset 55690 d73949233c2e
parent 55549 5c40782f68b3
child 55691 aeba7cd45400
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 15:38:21 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 16:08:38 2014 +0100
     1.3 @@ -177,6 +177,16 @@
     1.4        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
     1.5      }
     1.6  
     1.7 +  def stretch_point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     1.8 +  {
     1.9 +    val range = point_range(buffer, offset)
    1.10 +    val left = point_range(buffer, range.start - 1)
    1.11 +    val right = point_range(buffer, range.stop)
    1.12 +    val range1 = range.try_join(left) getOrElse range
    1.13 +    val range2 = range1.try_join(right) getOrElse range1
    1.14 +    range2
    1.15 +  }
    1.16 +
    1.17  
    1.18    /* visible text range */
    1.19