more navigator positions, after BufferUpdate.LOADED and Buffer.CARET_POSITIONED (see also e48b3ddc4810);

--- a/Admin/components/components.sha1	Thu Apr 24 09:16:33 2025 +0200
+++ b/Admin/components/components.sha1	Thu Apr 24 12:23:37 2025 +0200
@@ -274,6 +274,7 @@
 23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz
 a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz
 07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz
+995ac4cd9086e1647f1628988884c7c135123965 jedit-20250424.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz

--- a/Admin/components/main	Thu Apr 24 09:16:33 2025 +0200
+++ b/Admin/components/main	Thu Apr 24 12:23:37 2025 +0200
@@ -15,7 +15,7 @@
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250423
+jedit-20250424
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3

--- /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;