# HG changeset patch
# User wenzelm
# Date 1314714804 -7200
# Node ID 022509c908fb6c38af1588e5fd740f36b5547687
# Parent  479c070729921b5bf6c7d7284dad71cb4671633d
restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);

diff -r 479c07072992 -r 022509c908fb src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 30 16:04:26 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 30 16:33:24 2011 +0200
@@ -118,14 +118,17 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
+    val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
     Text.Perspective(
       for {
         i <- 0 until text_area.getVisibleLines
         val start = text_area.getScreenLineStartOffset(i)
         val stop = text_area.getScreenLineEndOffset(i)
         if start >= 0 && stop >= 0
+        val range <- buffer_range.try_restrict(Text.Range(start, stop))
+        if !range.is_singularity
       }
-      yield Text.Range(start, stop))
+      yield range)
   }
 
   private def update_perspective = new TextAreaExtension