author | wenzelm |
Wed, 10 Jun 2020 19:59:12 +0200 | |
changeset 71932 | 65fd0f032a75 |
parent 69838 | 4419d4d675c3 |
child 72247 | c06260b7152c |
permissions | -rw-r--r-- |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
1 |
diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
2 |
--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-05-20 11:10:12.000000000 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
3 |
+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-06-10 15:37:37.310005209 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
4 |
@@ -1194,6 +1194,7 @@ |
69765 | 5 |
VFSFile[] selectedFiles = browserView.getSelectedFiles(); |
6 |
||
7 |
Buffer buffer = null; |
|
8 |
+ String bufferMarker = null; |
|
9 |
||
10 |
check_selected: |
|
11 |
for (VFSFile file : selectedFiles) |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
12 |
@@ -1243,7 +1244,10 @@ |
69765 | 13 |
} |
14 |
||
15 |
if (_buffer != null) |
|
16 |
+ { |
|
17 |
buffer = _buffer; |
|
18 |
+ bufferMarker = file.getPathMarker(); |
|
19 |
+ } |
|
20 |
} |
|
21 |
// otherwise if a file is selected in OPEN_DIALOG or |
|
22 |
// SAVE_DIALOG mode, just let the listener(s) |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
23 |
@@ -1252,21 +1256,30 @@ |
69765 | 24 |
|
25 |
if(buffer != null) |
|
26 |
{ |
|
27 |
+ View gotoView = null; |
|
28 |
+ |
|
29 |
switch(mode) |
|
30 |
{ |
|
31 |
case M_OPEN: |
|
32 |
view.setBuffer(buffer); |
|
33 |
+ gotoView = view; |
|
34 |
break; |
|
35 |
case M_OPEN_NEW_VIEW: |
|
36 |
- jEdit.newView(view,buffer,false); |
|
37 |
+ gotoView = jEdit.newView(view,buffer,false); |
|
38 |
break; |
|
39 |
case M_OPEN_NEW_PLAIN_VIEW: |
|
40 |
- jEdit.newView(view,buffer,true); |
|
41 |
+ gotoView = jEdit.newView(view,buffer,true); |
|
42 |
break; |
|
43 |
case M_OPEN_NEW_SPLIT: |
|
44 |
view.splitHorizontally().setBuffer(buffer); |
|
45 |
+ gotoView = view; |
|
46 |
break; |
|
47 |
} |
|
48 |
+ |
|
49 |
+ if (gotoView != null && bufferMarker != null) |
|
50 |
+ { |
|
51 |
+ jEdit.gotoMarker(gotoView, buffer, bufferMarker); |
|
52 |
+ } |
|
53 |
} |
|
54 |
||
55 |
Object[] listeners = listenerList.getListenerList(); |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
56 |
diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
57 |
--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-05-20 11:10:11.000000000 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
58 |
+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-06-10 15:37:37.314005109 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
59 |
@@ -302,6 +302,12 @@ |
69765 | 60 |
} |
61 |
} //}}} |
|
62 |
||
63 |
+ //{{{ getPathMarker() method (for jEdit.gotoMarker) |
|
64 |
+ public String getPathMarker() |
|
65 |
+ { |
|
66 |
+ return null; |
|
67 |
+ } //}}} |
|
68 |
+ |
|
69 |
//{{{ getPath() method |
|
70 |
public String getPath() |
|
71 |
{ |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
72 |
diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
73 |
--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-05-26 16:55:37.000000000 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
74 |
+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-06-10 15:37:37.314005109 +0200 |
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
75 |
@@ -4242,7 +4242,7 @@ |
69765 | 76 |
} //}}} |
77 |
||
78 |
//{{{ gotoMarker() method |
|
79 |
- private static void gotoMarker(final View view, final Buffer buffer, |
|
80 |
+ public static void gotoMarker(final View view, final Buffer buffer, |
|
81 |
final String marker) |
|
82 |
{ |
|
83 |
AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() |