src/Tools/jEdit/patches/vfs_marker

updated to jedit-5.6pre1 (repository version 25349);

+
−diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
+
−--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-05-20 11:10:12.000000000 +0200
+
−+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-06-10 15:37:37.310005209 +0200
+
−@@ -1194,6 +1194,7 @@
+
− 		VFSFile[] selectedFiles = browserView.getSelectedFiles();
+
− 
+
− 		Buffer buffer = null;
+
−+		String bufferMarker = null;
+
− 
+
− check_selected:
+
− 		for (VFSFile file : selectedFiles)
+
−@@ -1243,7 +1244,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)
+
−@@ -1252,21 +1256,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 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
+
−--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java	2020-05-20 11:10:11.000000000 +0200
+
−+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2020-06-10 15:37:37.314005109 +0200
+
−@@ -302,6 +302,12 @@
+
− 		}
+
− 	} //}}}
+
− 
+
−+	//{{{ getPathMarker() method (for jEdit.gotoMarker)
+
−+	public String getPathMarker()
+
−+	{
+
−+		return null;
+
−+	} //}}}
+
−+
+
− 	//{{{ getPath() method
+
− 	public String getPath()
+
− 	{
+
−diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java
+
−--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java	2020-05-26 16:55:37.000000000 +0200
+
−+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2020-06-10 15:37:37.314005109 +0200
+
−@@ -4242,7 +4242,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()