# HG changeset patch
# User wenzelm
# Date 1742937807 -3600
# Node ID c597898ff51b48781d9525c3181966f9d1b61c4c
# Parent  f3fbe96bd7185eafdbf30205654f1f6249192344
clarified signature;

diff -r f3fbe96bd718 -r c597898ff51b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 25 21:24:39 2025 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 25 22:23:27 2025 +0100
@@ -18,7 +18,7 @@
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
 
 
 object Document_Model {
@@ -568,6 +568,8 @@
       PIDE.editor.invoke()
     }
 
+    val listener: BufferListener = JEdit_Lib.buffer_listener((_, e) => edit(List(e)))
+
 
     // blob
 
@@ -621,31 +623,6 @@
   def untyped_data: AnyRef = buffer_state.untyped_data
 
 
-  /* buffer listener */
-
-  private val buffer_listener: BufferListener = new BufferAdapter {
-    override def contentInserted(
-      buffer: JEditBuffer,
-      start_line: Int,
-      offset: Int,
-      num_lines: Int,
-      length: Int
-    ): Unit = {
-      buffer_state.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
-    }
-
-    override def preContentRemoved(
-      buffer: JEditBuffer,
-      start_line: Int,
-      offset: Int,
-      num_lines: Int,
-      removed_length: Int
-    ): Unit = {
-      buffer_state.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
-    }
-  }
-
-
   /* syntax */
 
   def syntax_changed(): Unit = {
@@ -681,7 +658,7 @@
             Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
 
-    buffer.addBufferListener(buffer_listener)
+    buffer.addBufferListener(buffer_state.listener)
     init_token_marker()
 
     this
@@ -691,7 +668,7 @@
   /* exit */
 
   def exit(): File_Model = GUI_Thread.require {
-    buffer.removeBufferListener(buffer_listener)
+    buffer.removeBufferListener(buffer_state.listener)
     init_token_marker()
 
     File_Model.init(session,
diff -r f3fbe96bd718 -r c597898ff51b src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Mar 25 21:24:39 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Mar 25 22:23:27 2025 +0100
@@ -23,7 +23,7 @@
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
 import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
-import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
+import org.gjt.sp.jedit.buffer.{BufferListener, BufferAdapter, JEditBuffer, LineManager}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection, AntiAlias}
 
 
@@ -403,6 +403,17 @@
     }
 
 
+  /* buffer event handling */
+
+  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)))
+      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)))
+    }
+
+
   /* key event handling */
 
   def request_focus_view(alt_view: View = null): Unit = {