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);
authorwenzelm
Tue, 30 Aug 2011 16:33:24 +0200
changeset 44583 022509c908fb
parent 44582 479c07072992
child 44600 426834f253c8
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);
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