69 //{{{ getPath() method |
69 //{{{ getPath() method |
70 public String getPath() |
70 public String getPath() |
71 { |
71 { |
72 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java |
72 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java |
73 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200 |
73 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200 |
74 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2025-04-02 21:46:10.377166514 +0200 |
74 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2024-10-29 11:50:54.062016616 +0100 |
75 @@ -1553,7 +1553,7 @@ |
|
76 { |
|
77 if (arg == null) |
|
78 continue; |
|
79 - else if (arg.startsWith("+line:") || arg.startsWith("+marker:")) |
|
80 + else if (arg.startsWith("+offset:") || arg.startsWith("+line:") || arg.startsWith("+marker:")) |
|
81 { |
|
82 if (lastBuffer != null) |
|
83 gotoMarker(view, lastBuffer, arg); |
|
84 @@ -4233,7 +4233,7 @@ |
75 @@ -4233,7 +4233,7 @@ |
85 } //}}} |
76 } //}}} |
86 |
77 |
87 //{{{ gotoMarker() method |
78 //{{{ gotoMarker() method |
88 - private static void gotoMarker(final View view, final Buffer buffer, |
79 - private static void gotoMarker(final View view, final Buffer buffer, |
89 + public static void gotoMarker(final View view, final Buffer buffer, |
80 + public static void gotoMarker(final View view, final Buffer buffer, |
90 final String marker) |
81 final String marker) |
91 { |
82 { |
92 AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() |
83 AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() |
93 @@ -4243,8 +4243,27 @@ |
|
94 { |
|
95 int pos; |
|
96 |
|
97 + // Handle offset |
|
98 + if(marker.startsWith("+offset:")) |
|
99 + { |
|
100 + try |
|
101 + { |
|
102 + String arg = marker.substring(8); |
|
103 + int offset = parseInt(arg); |
|
104 + if (0 <= offset && offset <= buffer.getLength()) { |
|
105 + pos = offset; |
|
106 + } |
|
107 + else { |
|
108 + return; |
|
109 + } |
|
110 + } |
|
111 + catch(Exception e) |
|
112 + { |
|
113 + return; |
|
114 + } |
|
115 + } |
|
116 // Handle line number |
|
117 - if(marker.startsWith("+line:")) |
|
118 + else if(marker.startsWith("+line:")) |
|
119 { |
|
120 try |
|
121 { |
|