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);
1.1 --- a/src/Tools/jEdit/src/document_view.scala Tue Aug 30 16:04:26 2011 +0200
1.2 +++ b/src/Tools/jEdit/src/document_view.scala Tue Aug 30 16:33:24 2011 +0200
1.3 @@ -118,14 +118,17 @@
1.4 def perspective(): Text.Perspective =
1.5 {
1.6 Swing_Thread.require()
1.7 + val buffer_range = Text.Range(0, (model.buffer.getLength - 1) max 0)
1.8 Text.Perspective(
1.9 for {
1.10 i <- 0 until text_area.getVisibleLines
1.11 val start = text_area.getScreenLineStartOffset(i)
1.12 val stop = text_area.getScreenLineEndOffset(i)
1.13 if start >= 0 && stop >= 0
1.14 + val range <- buffer_range.try_restrict(Text.Range(start, stop))
1.15 + if !range.is_singularity
1.16 }
1.17 - yield Text.Range(start, stop))
1.18 + yield range)
1.19 }
1.20
1.21 private def update_perspective = new TextAreaExtension