src/Tools/jEdit/patches/position_changing

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/position_changing	Thu Apr 24 12:23:37 2025 +0200
@@ -0,0 +1,24 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java	2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java	2025-04-24 11:45:26.809862122 +0200
+@@ -43,6 +43,7 @@
+ import org.gjt.sp.jedit.msg.BufferChanging;
+ import org.gjt.sp.jedit.msg.BufferUpdate;
+ import org.gjt.sp.jedit.msg.EditPaneUpdate;
++import org.gjt.sp.jedit.msg.PositionChanging;
+ import org.gjt.sp.jedit.msg.PropertiesChanged;
+ import org.gjt.sp.jedit.options.GeneralOptionPane;
+ import org.gjt.sp.jedit.options.GutterOptionPane;
+@@ -380,9 +381,11 @@
+ 		buffer.unsetProperty(Buffer.CARET_POSITIONED);
+ 
+ 
+-		if(caret != -1)
++		if(caret != -1) {
+ 			textArea.setCaretPosition(Math.min(caret,
+ 				buffer.getLength()));
++			EditBus.send(new PositionChanging(this));
++		}
+ 
+ 		// set any selections
+ 		Selection[] selection = caretInfo.selection;