src/Tools/jEdit/patches/vfs_marker

support for jEdit.openFiles with "+offset:" specification --- requires to update jedit component;

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	2024-10-29 11:50:54.058016686 +0100
@@ -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();
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()
 	{
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java	2024-08-03 19:53:14.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java	2025-04-02 21:46:10.377166514 +0200
@@ -1553,7 +1553,7 @@
 		{
 			if (arg == null)
 				continue;
-			else if (arg.startsWith("+line:") || arg.startsWith("+marker:"))
+			else if (arg.startsWith("+offset:") || arg.startsWith("+line:") || arg.startsWith("+marker:"))
 			{
 				if (lastBuffer != null)
 					gotoMarker(view, lastBuffer, arg);
@@ -4233,7 +4233,7 @@
 	} //}}}
 
 	//{{{ gotoMarker() method
-	private static void gotoMarker(final View view, final Buffer buffer,
+	public static void gotoMarker(final View view, final Buffer buffer,
 		final String marker)
 	{
 		AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
@@ -4243,8 +4243,27 @@
 			{
 				int pos;
 
+				// Handle offset
+				if(marker.startsWith("+offset:"))
+				{
+					try
+					{
+						String arg = marker.substring(8);
+						int offset = parseInt(arg);
+						if (0 <= offset && offset <= buffer.getLength()) {
+							pos = offset;
+						}
+						else {
+							return;
+						}
+					}
+					catch(Exception e)
+					{
+						return;
+					}
+				}
 				// Handle line number
-				if(marker.startsWith("+line:"))
+				else if(marker.startsWith("+line:"))
 				{
 					try
 					{