# HG changeset patch
# User wenzelm
# Date 1730201415 -3600
# Node ID 07f64697408ecc8d4e860507e238ebaf128a60a4
# Parent  59994f7feace8427acfcb32cd1211f57c94f0ed8
update to jedit5.7.0;

diff -r 59994f7feace -r 07f64697408e src/Pure/Admin/component_jedit.scala
--- 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 =
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/accelerator_font
--- 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 {
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/docking
--- 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
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/extended_styles_brackets
--- 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 @@
  			}
  		}
  
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/folding
--- 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);
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/laf_fonts
--- 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
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/panel_font
--- 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);
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/props
--- 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
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/putenv
--- 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);
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/title
--- 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();
  
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/vfs_manager
--- 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)
  				{
diff -r 59994f7feace -r 07f64697408e src/Tools/jEdit/patches/vfs_marker
--- 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