--- 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
--- 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
--- 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 ***
--- 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
--- 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);
}
--- 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
--- 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 @@
}
}
--- 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();
--- 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\
--- 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);
--- 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();
--- 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)
--- 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 @@
} //}}}