more regular buffer_range, despite 47e8c8daccae;
more robust invalidate_range, which is relevant when editing at the end of the buffer (NB: last line offset by be outside actual buffer length);

--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 18:11:11 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 22:11:52 2014 +0100
@@ -155,12 +155,6 @@
     catch { case _: IndexOutOfBoundsException => None }
 
 
-  /* buffer range */
-
-  def buffer_range(buffer: JEditBuffer): Text.Range =
-    Text.Range(0, (buffer.getLength - 1) max 0)
-
-
   /* point range */
 
   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
@@ -179,7 +173,10 @@
     }
 
 
-  /* visible text range */
+  /* text ranges */
+
+  def buffer_range(buffer: JEditBuffer): Text.Range =
+    Text.Range(0, buffer.getLength)
 
   def visible_range(text_area: TextArea): Option[Text.Range] =
   {
@@ -197,9 +194,13 @@
   def invalidate_range(text_area: TextArea, range: Text.Range)
   {
     val buffer = text_area.getBuffer
-    text_area.invalidateLineRange(
-      buffer.getLineOfOffset(range.start),
-      buffer.getLineOfOffset(range.stop))
+    buffer_range(buffer).try_restrict(range) match {
+      case Some(range1) if !range1.is_singularity =>
+        text_area.invalidateLineRange(
+          buffer.getLineOfOffset(range1.start),
+          buffer.getLineOfOffset(range1.stop))
+      case _ =>
+    }
   }