equal
deleted
inserted
replaced
1 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 |
1 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java |
2 --- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200 |
2 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200 |
3 +++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-08 20:13:45.348505646 +0200 |
3 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2021-05-10 11:02:05.824257741 +0200 |
4 @@ -1194,6 +1194,7 @@ |
4 @@ -1194,6 +1194,7 @@ |
5 VFSFile[] selectedFiles = browserView.getSelectedFiles(); |
5 VFSFile[] selectedFiles = browserView.getSelectedFiles(); |
6 |
6 |
7 Buffer buffer = null; |
7 Buffer buffer = null; |
8 + String bufferMarker = null; |
8 + String bufferMarker = null; |
51 + jEdit.gotoMarker(gotoView, buffer, bufferMarker); |
51 + jEdit.gotoMarker(gotoView, buffer, bufferMarker); |
52 + } |
52 + } |
53 } |
53 } |
54 |
54 |
55 Object[] listeners = listenerList.getListenerList(); |
55 Object[] listeners = listenerList.getListenerList(); |
56 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 |
56 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java |
57 --- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200 |
57 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200 |
58 +++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-09-08 20:13:45.348505646 +0200 |
58 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2021-05-10 11:02:05.824257741 +0200 |
59 @@ -302,6 +302,12 @@ |
59 @@ -302,6 +302,12 @@ |
60 } |
60 } |
61 } //}}} |
61 } //}}} |
62 |
62 |
63 + //{{{ getPathMarker() method (for jEdit.gotoMarker) |
63 + //{{{ getPathMarker() method (for jEdit.gotoMarker) |
67 + } //}}} |
67 + } //}}} |
68 + |
68 + |
69 //{{{ getPath() method |
69 //{{{ getPath() method |
70 public String getPath() |
70 public String getPath() |
71 { |
71 { |
72 diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java |
72 diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java |
73 --- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200 |
73 --- jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200 |
74 +++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-09-08 20:13:45.348505646 +0200 |
74 +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2021-05-10 11:02:05.824257741 +0200 |
75 @@ -4242,7 +4242,7 @@ |
75 @@ -4242,7 +4242,7 @@ |
76 } //}}} |
76 } //}}} |
77 |
77 |
78 //{{{ gotoMarker() method |
78 //{{{ gotoMarker() method |
79 - private static void gotoMarker(final View view, final Buffer buffer, |
79 - private static void gotoMarker(final View view, final Buffer buffer, |