src/Tools/jEdit/src/jedit_lib.scala
changeset 50215 97959912840a
parent 50195 863b1dfc396c
child 50363 2f8dc9e65401
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -105,6 +105,13 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* get text */
     1.8 +
     1.9 +  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
    1.10 +    try { Some(buffer.getText(range.start, range.length)) }
    1.11 +    catch { case _: ArrayIndexOutOfBoundsException => None }
    1.12 +
    1.13 +
    1.14    /* point range */
    1.15  
    1.16    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =