1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 18:11:11 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 22:11:52 2014 +0100
     1.3 @@ -155,12 +155,6 @@
     1.4      catch { case _: IndexOutOfBoundsException => None }
     1.5  
     1.6  
     1.7 -  /* buffer range */
     1.8 -
     1.9 -  def buffer_range(buffer: JEditBuffer): Text.Range =
    1.10 -    Text.Range(0, (buffer.getLength - 1) max 0)
    1.11 -
    1.12 -
    1.13    /* point range */
    1.14  
    1.15    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
    1.16 @@ -179,7 +173,10 @@
    1.17      }
    1.18  
    1.19  
    1.20 -  /* visible text range */
    1.21 +  /* text ranges */
    1.22 +
    1.23 +  def buffer_range(buffer: JEditBuffer): Text.Range =
    1.24 +    Text.Range(0, buffer.getLength)
    1.25  
    1.26    def visible_range(text_area: TextArea): Option[Text.Range] =
    1.27    {
    1.28 @@ -197,9 +194,13 @@
    1.29    def invalidate_range(text_area: TextArea, range: Text.Range)
    1.30    {
    1.31      val buffer = text_area.getBuffer
    1.32 -    text_area.invalidateLineRange(
    1.33 -      buffer.getLineOfOffset(range.start),
    1.34 -      buffer.getLineOfOffset(range.stop))
    1.35 +    buffer_range(buffer).try_restrict(range) match {
    1.36 +      case Some(range1) if !range1.is_singularity =>
    1.37 +        text_area.invalidateLineRange(
    1.38 +          buffer.getLineOfOffset(range1.start),
    1.39 +          buffer.getLineOfOffset(range1.stop))
    1.40 +      case _ =>
    1.41 +    }
    1.42    }
    1.43  
    1.44