--- a/src/Pure/Admin/component_jedit.scala Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Pure/Admin/component_jedit.scala Tue Oct 29 12:30:15 2024 +0100
@@ -501,7 +501,7 @@
/** Isabelle tool wrappers **/
- val default_version = "5.6.0"
+ val default_version = "5.7.0"
def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
--- a/src/Tools/jEdit/patches/accelerator_font Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/accelerator_font Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2021-05-10 11:02:05.784257753 +0200
-@@ -1130,9 +1130,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-10-29 11:50:54.062016616 +0100
+@@ -1094,9 +1094,7 @@
return new Font("Monospaced", Font.PLAIN, 12);
}
else {
--- a/src/Tools/jEdit/patches/docking Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/docking Tue Oct 29 12:30:15 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2021-05-10 11:02:05.760257760 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-10-29 11:50:54.062016616 +0100
@@ -45,14 +45,15 @@
* @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
* @since jEdit 4.0pre1
--- a/src/Tools/jEdit/patches/extended_styles_brackets Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/extended_styles_brackets Tue Oct 29 12:30:15 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-04-25 12:56:22.208257322 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -36,10 +36,10 @@
protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
{
return size() > capacity;
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2023-11-20 15:31:55.825519645 +0100
-@@ -914,6 +914,11 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-10-29 11:50:54.066016546 +0100
+@@ -919,6 +919,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -51,7 +51,7 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-@@ -1622,8 +1627,8 @@
+@@ -1627,8 +1632,8 @@
}
// Scan backwards, trying to find a bracket
@@ -62,18 +62,9 @@
int count = 1;
char openBracket = '\0';
char closeBracket = '\0';
-@@ -6336,7 +6341,7 @@
- {
- int following = charBreaker.following(offset -
- index0Offset);
-- if (following == BreakIterator.DONE)
-+ if (following == BreakIterator.DONE || (Runtime.version().feature() >= 20 && following == offset - index0Offset))
- {
- // This means a end of line. Then it is
- // safe to assume 1 code unit is a character.
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100
@@ -115,6 +115,8 @@
case '⦄': if (direction != null) direction[0] = false; return '⦃';
case '⟪': if (direction != null) direction[0] = true; return '⟫';
@@ -83,10 +74,10 @@
default: return '\0';
}
} //}}}
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200
-@@ -344,8 +344,28 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-10-29 11:50:54.066016546 +0100
+@@ -357,8 +357,28 @@
}
}
--- a/src/Tools/jEdit/patches/folding Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/folding Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2021-05-10 11:02:05.776257756 +0200
-@@ -1968,29 +1968,23 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-10-29 11:50:54.062016616 +0100
+@@ -2054,29 +2054,23 @@
{
Segment seg = new Segment();
newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
--- a/src/Tools/jEdit/patches/laf_fonts Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/laf_fonts Tue Oct 29 12:30:15 2024 +0100
@@ -1,5 +1,6 @@
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2020-09-03 05:31:04.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2021-02-01 18:00:07.541681144 +0100
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-10-29 11:50:54.062016616 +0100
@@ -414,7 +414,9 @@
// adjust swing properties for button, menu, and label, and list and
@@ -11,3 +12,4 @@
// This is handled a little differently from other jEdit settings
// as this flag needs to be known very early in the
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- a/src/Tools/jEdit/patches/panel_font Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/panel_font Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2021-05-10 11:23:04.107511056 +0200
-@@ -52,6 +52,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-10-29 11:50:54.062016616 +0100
+@@ -53,6 +53,7 @@
import javax.swing.JComponent;
import javax.swing.JPanel;
import javax.swing.JPopupMenu;
@@ -9,7 +9,7 @@
import javax.swing.JToggleButton;
import javax.swing.UIManager;
import javax.swing.border.Border;
-@@ -163,6 +164,7 @@
+@@ -164,6 +165,7 @@
{
button = new JToggleButton();
button.setMargin(new Insets(1,1,1,1));
@@ -17,7 +17,7 @@
}
GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
button.setRequestFocusEnabled(false);
-@@ -690,8 +692,6 @@
+@@ -683,8 +685,6 @@
renderHints = new RenderingHints(
RenderingHints.KEY_ANTIALIASING,
RenderingHints.VALUE_ANTIALIAS_ON);
--- a/src/Tools/jEdit/patches/props Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/props Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props
---- jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props 2021-05-10 11:02:05.788257753 +0200
-@@ -1277,8 +1277,7 @@
+diff -ru jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props
+--- jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props 2024-08-03 19:53:22.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props 2024-10-29 11:50:54.066016546 +0100
+@@ -1282,8 +1282,7 @@
The most likely reason is that the JAR file is corrupt; try\n\
reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
for a full stack trace.
@@ -11,4 +11,3 @@
plugin-error.already-loaded=Two copies installed. Please remove one of the \
two copies.
plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
-Binary files jedit5.6.0/jedit.jar and jedit5.6.0-patched/jedit.jar differ
--- a/src/Tools/jEdit/patches/putenv Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/putenv Tue Oct 29 12:30:15 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2021-05-10 11:23:04.139510558 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-10-29 11:50:54.062016616 +0100
@@ -131,6 +131,21 @@
static final Pattern winPattern = Pattern.compile(winPatternString);
@@ -27,21 +27,21 @@
if (m.find())
{
String varName = m.group(2);
-- String expansion = System.getenv(varName);
+- String expansion = jEdit.systemManager.getenv(varName);
+ String expansion = getenv(varName);
if (expansion != null)
- return m.replaceFirst(expansion);
- }
-@@ -179,7 +194,7 @@
+ {
+ expansion = Matcher.quoteReplacement(expansion);
+@@ -182,7 +197,7 @@
return arg;
}
String varName = m.group(2);
-- String expansion = System.getenv(varName);
+- String expansion = jEdit.systemManager.getenv(varName);
+ String expansion = getenv(varName);
if (expansion == null) {
if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
expansion = jEdit.getSettingsDirectory();
-@@ -189,7 +204,7 @@
+@@ -192,7 +207,7 @@
varName = varName.toUpperCase();
String uparg = arg.toUpperCase();
m = p.matcher(uparg);
@@ -50,7 +50,7 @@
}
}
if (expansion != null) {
-@@ -1682,13 +1697,11 @@
+@@ -1674,13 +1689,11 @@
//{{{ VarCompressor constructor
VarCompressor()
{
@@ -65,3 +65,63 @@
{
String k = entry.getKey();
if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;
+diff -ru jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java
+--- jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-08-03 19:53:29.000000000 +0200
++++ jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-10-29 12:21:05.284840022 +0100
+@@ -167,56 +167,6 @@
+ }
+
+ @Test
+- public void expandVariablesEnvWindowsAsWindows() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(WINDOWS_NT);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
+- assertEquals(captor.getValue(), key);
+- }
+- @Test
+- public void expandVariablesEnvWindowsAsUnix() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
+- assertEquals(captor.getValue(), key);
+- }
+-
+- @Test
+- public void expandVariablesEnvUnix() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('$' + key));
+- assertEquals(captor.getValue(), key);
+- }
+-
+- @Test
+- public void expandVariablesEnvUnix2() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables("${" + key + '}'));
+- }
+-
+- @Test
+ public void expandVariablesEnvUnixNoMatch() throws Exception
+ {
+ updateOS(UNIX);
--- a/src/Tools/jEdit/patches/title Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/title Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java 2021-05-10 11:02:05.792257750 +0200
-@@ -1262,15 +1262,10 @@
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java 2024-10-29 11:50:54.066016546 +0100
+@@ -1264,15 +1264,10 @@
StringBuilder title = new StringBuilder();
--- a/src/Tools/jEdit/patches/vfs_manager Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/vfs_manager Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2021-05-10 11:02:05.808257746 +0200
-@@ -380,6 +380,18 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2024-10-29 11:50:54.062016616 +0100
+@@ -339,6 +339,18 @@
if(vfsUpdates.size() == 1)
{
--- a/src/Tools/jEdit/patches/vfs_marker Mon Oct 28 09:43:28 2024 +0100
+++ b/src/Tools/jEdit/patches/vfs_marker Tue Oct 29 12:30:15 2024 +0100
@@ -1,7 +1,7 @@
-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
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2021-05-10 11:02:05.824257741 +0200
-@@ -1194,6 +1194,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-10-29 11:50:54.058016686 +0100
+@@ -1195,6 +1195,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
Buffer buffer = null;
@@ -9,7 +9,7 @@
check_selected:
for (VFSFile file : selectedFiles)
-@@ -1243,7 +1244,10 @@
+@@ -1244,7 +1245,10 @@
}
if (_buffer != null)
@@ -20,7 +20,7 @@
}
// otherwise if a file is selected in OPEN_DIALOG or
// SAVE_DIALOG mode, just let the listener(s)
-@@ -1252,21 +1256,30 @@
+@@ -1253,21 +1257,30 @@
if(buffer != null)
{
@@ -53,9 +53,9 @@
}
Object[] listeners = listenerList.getListenerList();
-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
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2021-05-10 11:02:05.824257741 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
@@ -302,6 +302,12 @@
}
} //}}}
@@ -69,10 +69,10 @@
//{{{ getPath() method
public String getPath()
{
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2021-05-10 11:02:05.824257741 +0200
-@@ -4242,7 +4242,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2024-10-29 11:50:54.062016616 +0100
+@@ -4233,7 +4233,7 @@
} //}}}
//{{{ gotoMarker() method