diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/position_changing
--- a/src/Tools/jEdit/patches/position_changing	Wed May 14 11:31:23 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-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;