--- a/src/Tools/jEdit/patches/vfs_marker Wed May 21 15:09:48 2025 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2025-05-20 15:21:39.685949775 +0200
-@@ -1195,6 +1195,7 @@
- VFSFile[] selectedFiles = browserView.getSelectedFiles();
-
- Buffer buffer = null;
-+ String bufferMarker = null;
-
- check_selected:
- for (VFSFile file : selectedFiles)
-@@ -1244,7 +1245,10 @@
- }
-
- if (_buffer != null)
-+ {
- buffer = _buffer;
-+ bufferMarker = file.getPathMarker();
-+ }
- }
- // otherwise if a file is selected in OPEN_DIALOG or
- // SAVE_DIALOG mode, just let the listener(s)
-@@ -1253,21 +1257,30 @@
-
- if(buffer != null)
- {
-+ View gotoView = null;
-+
- switch(mode)
- {
- case M_OPEN:
- view.setBuffer(buffer);
-+ gotoView = view;
- break;
- case M_OPEN_NEW_VIEW:
-- jEdit.newView(view,buffer,false);
-+ gotoView = jEdit.newView(view,buffer,false);
- break;
- case M_OPEN_NEW_PLAIN_VIEW:
-- jEdit.newView(view,buffer,true);
-+ gotoView = jEdit.newView(view,buffer,true);
- break;
- case M_OPEN_NEW_SPLIT:
- view.splitHorizontally().setBuffer(buffer);
-+ gotoView = view;
- break;
- }
-+
-+ if (gotoView != null && bufferMarker != null)
-+ {
-+ jEdit.gotoMarker(gotoView, buffer, bufferMarker);
-+ }
- }
-
- Object[] listeners = listenerList.getListenerList();
-@@ -1751,7 +1764,7 @@
- //{{{ MenuButton constructor
- MenuButton()
- {
-- setIcon(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
-+ setIcon(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
- setHorizontalTextPosition(SwingConstants.LEADING);
-
- // setRequestFocusEnabled(false);
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
-@@ -302,6 +302,12 @@
- }
- } //}}}
-
-+ //{{{ getPathMarker() method (for jEdit.gotoMarker)
-+ public String getPathMarker()
-+ {
-+ return null;
-+ } //}}}
-+
- //{{{ getPath() method
- public String getPath()
- {