# HG changeset patch
# User wenzelm
# Date 1599592482 -7200
# Node ID c06260b7152c8f10f5710e6273c28a13edf17c16
# Parent  9c6787cfd70e640ffe6437a396e65b507cd61729
update to official jedit-5.6.0;

diff -r 9c6787cfd70e -r c06260b7152c Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Sep 08 15:30:37 2020 +0100
+++ b/Admin/components/components.sha1	Tue Sep 08 21:14:42 2020 +0200
@@ -171,6 +171,7 @@
 1e53598a02ec8d8736b15f480cbe2c84767a7827  jedit_build-20190508.tar.gz
 b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac  jedit_build-20190717.tar.gz
 1c753beb93e92e95e99e8ead23a68346bd1af44a  jedit_build-20200610.tar.gz
+533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
diff -r 9c6787cfd70e -r c06260b7152c Admin/components/main
--- a/Admin/components/main	Tue Sep 08 15:30:37 2020 +0100
+++ b/Admin/components/main	Tue Sep 08 21:14:42 2020 +0200
@@ -6,7 +6,7 @@
 e-2.0-3
 isabelle_fonts-20190717
 jdk-11.0.5+10
-jedit_build-20200610
+jedit_build-20200908
 jfreechart-1.5.0
 jortho-1.0-2
 kodkodi-1.5.6
diff -r 9c6787cfd70e -r c06260b7152c NEWS
--- a/NEWS	Tue Sep 08 15:30:37 2020 +0100
+++ b/NEWS	Tue Sep 08 21:14:42 2020 +0200
@@ -24,8 +24,8 @@
 collection and sharing of live data on the ML heap. It also includes
 information about the Java Runtime system.
 
-* Update to jedit-5.6pre1, the latest pre-release. This version works
-properly on macOS by default, without the special MacOSX plugin.
+* Update to jedit-5.6.0, the latest release. This version works properly
+on macOS by default, without the special MacOSX plugin.
 
 
 *** Document preparation ***
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Sep 08 21:14:42 2020 +0200
@@ -390,7 +390,7 @@
 
   target_shasum > "$TARGET_SHASUM"
 
-  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6pre1manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
+  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
   cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes"
   cat > "$TARGET_DIR/doc/Contents" <<EOF
 Original jEdit Documentation
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/accelerator_font
--- a/src/Tools/jEdit/patches/accelerator_font	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/accelerator_font	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java	2020-05-20 11:10:13.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2020-06-10 15:30:42.744707440 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java	2020-09-08 20:13:23.561140312 +0200
 @@ -1130,9 +1130,7 @@
  				return new Font("Monospaced", Font.PLAIN, 12);
  			}
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/docking
--- a/src/Tools/jEdit/patches/docking	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/docking	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-05-20 11:10:10.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-06-10 15:33:52.388038983 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-08 20:13:23.565140195 +0200
 @@ -45,14 +45,15 @@
   * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
   * @since jEdit 4.0pre1
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/extended_styles
--- a/src/Tools/jEdit/patches/extended_styles	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/extended_styles	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2020-06-09 17:01:03.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2020-06-10 15:38:59.771992636 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-08 20:13:23.565140195 +0200
 @@ -332,9 +332,9 @@
  	//{{{ Package private members
  
@@ -13,7 +13,8 @@
  	//}}}
  
  	//{{{ Chunk constructor
-@@ -585,7 +585,7 @@
+@@ -584,8 +584,8 @@
+ 	// this is either style.getBackgroundColor() or
  	// styles[defaultID].getBackgroundColor()
  	private Color background;
 -	private char[] chars;
@@ -23,9 +24,9 @@
  	private GlyphData glyphData;
  	//}}}
  
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2020-05-20 11:10:10.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2020-06-10 15:38:03.605353644 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-08 20:13:23.569140077 +0200
 @@ -914,6 +914,11 @@
  		return chunkCache.getLineInfo(screenLine).physicalLine;
  	} //}}}
@@ -38,9 +39,9 @@
  	//{{{ getScreenLineOfOffset() method
  	/**
  	 * Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2020-05-20 11:10:13.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2020-06-10 16:10:50.165837982 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2020-09-03 05:31:09.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2020-09-08 20:13:23.569140077 +0200
 @@ -344,8 +344,28 @@
  			}
  		}
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/folding
--- a/src/Tools/jEdit/patches/folding	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/folding	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java	2020-05-20 11:10:12.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2020-06-10 16:03:10.547355787 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2020-09-08 20:13:23.573139959 +0200
 @@ -1968,29 +1968,23 @@
  			{
  				Segment seg = new Segment();
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/props
--- a/src/Tools/jEdit/patches/props	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/props	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/jedit/localization/jedit_en.props 5.6pre1/jEdit-patched/org/jedit/localization/jedit_en.props
---- 5.6pre1/jEdit-orig/org/jedit/localization/jedit_en.props	2019-12-22 22:03:35.000000000 +0100
-+++ 5.6pre1/jEdit-patched/org/jedit/localization/jedit_en.props	2020-06-10 15:36:37.051536302 +0200
+diff -ru 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props
+--- 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props	2020-09-03 05:31:10.000000000 +0200
++++ 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props	2020-09-08 20:13:35.644786809 +0200
 @@ -1277,8 +1277,7 @@
  	The most likely reason is that the JAR file is corrupt; try\n\
  	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/putenv
--- a/src/Tools/jEdit/patches/putenv	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/putenv	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java	2020-06-09 22:58:00.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2020-06-10 15:36:56.603033473 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2020-09-08 20:13:35.648786692 +0200
 @@ -131,6 +131,21 @@
  	static final Pattern winPattern = Pattern.compile(winPatternString);
  
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/title
--- a/src/Tools/jEdit/patches/title	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/title	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/View.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/View.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/View.java	2020-06-10 14:07:09.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/View.java	2020-06-10 15:37:09.546703839 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java	2020-09-08 20:13:35.652786577 +0200
 @@ -1262,15 +1262,10 @@
  
  		StringBuilder title = new StringBuilder();
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/vfs_manager
--- a/src/Tools/jEdit/patches/vfs_manager	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/vfs_manager	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java	2020-05-20 11:10:11.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2020-06-10 15:37:21.842393040 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java	2020-09-03 05:31:03.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java	2020-09-08 20:13:35.656786460 +0200
 @@ -380,6 +380,18 @@
  
  				if(vfsUpdates.size() == 1)
diff -r 9c6787cfd70e -r c06260b7152c src/Tools/jEdit/patches/vfs_marker
--- a/src/Tools/jEdit/patches/vfs_marker	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/vfs_marker	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-05-20 11:10:12.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-06-10 15:37:37.310005209 +0200
+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
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-09-08 20:13:45.348505646 +0200
 @@ -1194,6 +1194,7 @@
  		VFSFile[] selectedFiles = browserView.getSelectedFiles();
  
@@ -53,9 +53,9 @@
  		}
  
  		Object[] listeners = listenerList.getListenerList();
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java	2020-05-20 11:10:11.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2020-06-10 15:37:37.314005109 +0200
+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
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java	2020-09-03 05:31:03.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2020-09-08 20:13:45.348505646 +0200
 @@ -302,6 +302,12 @@
  		}
  	} //}}}
@@ -69,9 +69,9 @@
  	//{{{ getPath() method
  	public String getPath()
  	{
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java	2020-05-26 16:55:37.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2020-06-10 15:37:37.314005109 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2020-09-08 20:13:45.348505646 +0200
 @@ -4242,7 +4242,7 @@
  	} //}}}