|
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-08 20:13:45.348505646 +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.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-09-08 20:13:45.348505646 +0200
@@ -302,6 +302,12 @@
}
} //}}}
+ //{{{ getPathMarker() method (for jEdit.gotoMarker)
+ public String getPathMarker()
+ {
+ return null;
+ } //}}}
+
//{{{ getPath() method
public String getPath()
{
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-09-08 20:13:45.348505646 +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()
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
