# HG changeset patch
# User wenzelm
# Date 1743791517 -7200
# Node ID 96ec907364d75fadb65c55b6ff9c147d37d00762
# Parent  af78b84151ed3b1d23f0d5a8c3035d8b1eec4d89
more robust: make double-sure that get_text does not crash (see on non-existent file);

diff -r af78b84151ed -r 96ec907364d7 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Apr 04 19:52:52 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Apr 04 20:31:57 2025 +0200
@@ -405,12 +405,19 @@
 
   /* buffer event handling */
 
+  private def buffer_edit(ins: Boolean, buf: JEditBuffer, i: Text.Offset, n: Int): Text.Edit = {
+    val try_range = Text.Range(i, i + n.max(0)).try_restrict(buffer_range(buf))
+    val edit_range = try_range.getOrElse(Text.Range.zero)
+    val edit_text = try_range.flatMap(get_text(buf, _)).getOrElse("")
+    Text.Edit.make(ins, edit_range.start, edit_text)
+  }
+
   def buffer_listener(handle: (Buffer, Text.Edit) => Unit): BufferListener =
     new BufferAdapter {
       override def contentInserted(buf: JEditBuffer, line: Int, i: Int, lines: Int, n: Int): Unit =
-        handle(buf.asInstanceOf[Buffer], Text.Edit.insert(i, buf.getText(i, n)))
+        handle(buf.asInstanceOf[Buffer], buffer_edit(true, buf, i, n))
       override def preContentRemoved(buf: JEditBuffer, line: Int, i: Int, lines: Int, n: Int): Unit =
-        handle(buf.asInstanceOf[Buffer], Text.Edit.remove(i, buf.getText(i, n)))
+        handle(buf.asInstanceOf[Buffer], buffer_edit(false, buf, i, n))
     }