--- a/Admin/components/components.sha1 Wed Jun 10 15:55:41 2020 +0200
+++ b/Admin/components/components.sha1 Wed Jun 10 19:59:12 2020 +0200
@@ -170,6 +170,7 @@
ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
+1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.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 Wed Jun 10 15:55:41 2020 +0200
+++ b/Admin/components/main Wed Jun 10 19:59:12 2020 +0200
@@ -6,7 +6,7 @@
e-2.0-3
isabelle_fonts-20190717
jdk-11.0.5+10
-jedit_build-20190717
+jedit_build-20200610
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.2-1
--- a/NEWS Wed Jun 10 15:55:41 2020 +0200
+++ b/NEWS Wed Jun 10 19:59:12 2020 +0200
@@ -7,6 +7,12 @@
New in this Isabelle version
----------------------------
+*** Isabelle/jEdit Prover IDE ***
+
+* Update to jedit-5.6pre1, the latest pre-release. This version works
+properly on macOS by default, without the special MacOSX plugin.
+
+
*** Document preparation ***
* Antiquotation @{bash_function} refers to GNU bash functions that are
--- a/src/Pure/Admin/build_release.scala Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Pure/Admin/build_release.scala Wed Jun 10 19:59:12 2020 +0200
@@ -547,8 +547,7 @@
File.read(isabelle_target + jedit_props)
.replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
- .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
- .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
+ .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// MacOS application bundle
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jun 10 19:59:12 2020 +0200
@@ -261,7 +261,6 @@
"ErrorList.jar"
"Highlight.jar"
"kappalayout.jar"
- "MacOSX.jar"
"Navigator.jar"
"SideKick.jar"
"idea-icons.jar"
@@ -390,12 +389,12 @@
target_shasum > "$TARGET_SHASUM"
- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.5.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
+ cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6pre1manual-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
- jedit-manual jEdit 5.5 User's Guide
- jedit-changes jEdit 5.5 Version History
+ jedit-manual jEdit 5.6 User's Guide
+ jedit-changes jEdit 5.6 Version History
EOF
--- a/src/Tools/jEdit/patches/accelerator_font Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/accelerator_font Wed Jun 10 19:59:12 2020 +0200
@@ -1,11 +1,13 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2018-04-09 01:58:07.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2019-02-24 12:19:52.134389619 +0100
-@@ -1172,7 +1172,7 @@
+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
+@@ -1130,9 +1130,7 @@
return new Font("Monospaced", Font.PLAIN, 12);
}
else {
-- Font font2 = new Font("Lucida Sans Typewriter", Font.PLAIN, font1.getSize());
+- Font font2 =
+- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
+- Font.PLAIN, font1.getSize());
+ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
FontRenderContext frc = new FontRenderContext(null, true, false);
float scale =
--- a/src/Tools/jEdit/patches/brackets Wed Jun 10 15:55:41 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
---- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-07-17 21:36:43.985183582 +0200
-@@ -1625,8 +1630,8 @@
- }
-
- // Scan backwards, trying to find a bracket
-- String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
-- String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄";
-+ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
-+ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
- int count = 1;
- char openBracket = '\0';
- char closeBracket = '\0';
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2018-04-09 01:58:07.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2019-07-17 21:44:15.545431576 +0200
-@@ -113,6 +113,8 @@
- case '⟧': if (direction != null) direction[0] = false; return '⟦';
- case '⦃': if (direction != null) direction[0] = true; return '⦄';
- case '⦄': if (direction != null) direction[0] = false; return '⦃';
-+ case '⟪': if (direction != null) direction[0] = true; return '⟫';
-+ case '⟫': if (direction != null) direction[0] = false; return '⟪';
- default: return '\0';
- }
- } //}}}
--- a/src/Tools/jEdit/patches/docking Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/docking Wed Jun 10 19:59:12 2020 +0200
@@ -1,25 +1,16 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2018-04-09 01:56:46.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2019-02-24 12:20:02.862430679 +0100
-@@ -35,7 +35,7 @@
- import javax.swing.Box;
- import javax.swing.BoxLayout;
- import javax.swing.JButton;
--import javax.swing.JFrame;
-+import javax.swing.JDialog;
- import javax.swing.JPopupMenu;
- import javax.swing.JSeparator;
- import javax.swing.SwingUtilities;
-@@ -51,7 +51,7 @@
- * @version $Id: FloatingWindowContainer.java 24411 2016-06-19 11:02:53Z kerik-sf $
+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
+@@ -45,14 +45,15 @@
+ * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
* @since jEdit 4.0pre1
*/
--public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
-+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
- PropertyChangeListener
- {
- String dockableName = null;
-@@ -59,6 +59,8 @@
+-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
+-{
++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
+ private String dockableName;
+
+ //{{{ FloatingWindowContainer constructor
public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
boolean clone)
{
@@ -28,7 +19,7 @@
this.dockableWindowManager = dockableWindowManager;
dockableWindowManager.addPropertyChangeListener(this);
-@@ -94,7 +96,6 @@
+@@ -87,7 +88,6 @@
pack();
Container parent = dockableWindowManager.getView();
GUIUtilities.loadGeometry(this, parent, dockableName);
@@ -36,7 +27,7 @@
KeyListener listener = dockableWindowManager.closeListener(dockableName);
addKeyListener(listener);
getContentPane().addKeyListener(listener);
-@@ -161,8 +162,11 @@
+@@ -154,8 +154,11 @@
@Override
public void dispose()
{
--- a/src/Tools/jEdit/patches/extended_styles Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/extended_styles Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2018-04-09 01:57:24.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2019-02-24 12:32:09.336643045 +0100
-@@ -322,9 +322,9 @@
+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
+@@ -332,9 +332,9 @@
//{{{ Package private members
//{{{ Instance variables
@@ -13,19 +13,20 @@
//}}}
//{{{ Chunk constructor
-@@ -572,7 +572,7 @@
- // this is either style.getBackgroundColor() or
+@@ -585,7 +585,7 @@
// styles[defaultID].getBackgroundColor()
private Color background;
+- private char[] chars;
- private String str;
++ public char[] chars;
+ public String str;
- private GlyphVector[] glyphs;
+ private GlyphData glyphData;
//}}}
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-02-24 12:20:10.550459878 +0100
-@@ -917,6 +917,11 @@
+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
+@@ -914,6 +914,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -37,15 +38,20 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2018-04-09 01:58:37.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2019-02-24 12:20:10.550459878 +0100
-@@ -200,7 +200,24 @@
- {
- return loadStyles(family,size,true);
- }
--
-+
+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
+@@ -344,8 +344,28 @@
+ }
+ }
+
+- return styles;
++ styles[0] =
++ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
++ null, new Font(family, 0, size));
++ return _styleExtender.extendStyles(styles);
+ } //}}}
+
+ /**
+ * Extended styles derived from the user-specified style array.
+ */
@@ -63,21 +69,5 @@
+ _styleExtender = ext;
+ }
+
- /**
- * Loads the syntax styles from the properties, giving them the specified
- * base font family and size.
-@@ -230,9 +247,11 @@
- Log.log(Log.ERROR,StandardUtilities.class,e);
- }
- }
--
-- return styles;
-+ styles[0] =
-+ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
-+ null, new Font(family, 0, size));
-+ return _styleExtender.extendStyles(styles);
- } //}}}
--
-+
private SyntaxUtilities(){}
}
--- a/src/Tools/jEdit/patches/favorites Wed Jun 10 15:55:41 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/io/FavoritesVFS.java 2018-04-09 01:57:13.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/FavoritesVFS.java 2019-02-24 12:20:21.702501903 +0100
-@@ -70,7 +70,8 @@
- public VFSFile[] _listFiles(Object session, String url,
- Component comp)
- {
-- return getFavorites();
-+ if (url.equals(PROTOCOL + ':')) return getFavorites();
-+ else return null;
- } //}}}
-
- //{{{ _getFile() method
--- a/src/Tools/jEdit/patches/folding Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/folding Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2018-04-09 01:57:06.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2019-02-24 12:20:30.594535134 +0100
-@@ -1961,29 +1961,23 @@
+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
+@@ -1968,29 +1968,23 @@
{
Segment seg = new Segment();
newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
@@ -32,13 +32,13 @@
- for (Integer foldLevel: precedingFoldLevels)
- {
- j--;
-- lineMgr.setFoldLevel(j,foldLevel.intValue());
+- lineMgr.setFoldLevel(j, foldLevel);
- }
- if (j < firstUpdatedFoldLevel)
- firstUpdatedFoldLevel = j;
- }
+ j--;
-+ lineMgr.setFoldLevel(j,foldLevel.intValue());
++ lineMgr.setFoldLevel(j, foldLevel);
}
+ if (j < firstUpdatedFoldLevel)
+ firstUpdatedFoldLevel = j;
--- a/src/Tools/jEdit/patches/glyphvector Wed Jun 10 15:55:41 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2018-04-09 01:57:24.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2019-02-24 12:32:09.336643045 +0100
-@@ -655,6 +655,10 @@
- // instance to the char array.
- font.layoutGlyphVector(frc, EMPTY_TEXT, 0, 0, flags);
-
-+ if ((result.getLayoutFlags() & GlyphVector.FLAG_COMPLEX_GLYPHS) != 0) {
-+ result = font.createGlyphVector(frc, new String(text, start, end - start));
-+ }
-+
- return result;
- } // }}}
-
--- a/src/Tools/jEdit/patches/macosx Wed Jun 10 15:55:41 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,197 +0,0 @@
-diff -ru MacOSX-trunk-r24891/build.properties MacOSX-trunk/build.properties
---- MacOSX-trunk-r24891/build.properties 2018-10-20 11:45:32.000000000 +0200
-+++ MacOSX-trunk/build.properties 2019-05-08 17:07:07.001576716 +0200
-@@ -1,3 +1,6 @@
- build.support=../build-support-trunk
- jedit.install.dir=../jedit-trunk/build
- install.dir=${jedit.install.dir}/jars
-+compiler.target=1.9
-+compiler.source=1.9
-+compiler.extdirs=
-diff -ru MacOSX-trunk-r24891/CHANGES.txt MacOSX-trunk/CHANGES.txt
---- MacOSX-trunk-r24891/CHANGES.txt 2013-09-24 01:12:13.000000000 +0200
-+++ MacOSX-trunk/CHANGES.txt 2019-05-08 17:07:07.001576716 +0200
-@@ -1,3 +1,6 @@
-+Mac OS X Plugin 1.4 [Makarius]
-+- Updates for Java 9: use java.awt.Desktop instead of old com.apple.eawt.Application / OSXAdapter.
-+
- Mac OS X Plugin 1.3 [Alan Ezust]
- - Updates for Java 7 and jEdit 5.2
- - Got rid of alternative dispatcher stuff which was workaround for Java 5 bugs.
-diff -ru MacOSX-trunk-r24891/docs/MacOSX.html MacOSX-trunk/docs/MacOSX.html
---- MacOSX-trunk-r24891/docs/MacOSX.html 2013-09-19 19:42:51.000000000 +0200
-+++ MacOSX-trunk/docs/MacOSX.html 2019-05-08 17:07:07.001576716 +0200
-@@ -16,8 +16,8 @@
- <td valign="TOP"><strong><font size="+2">jEdit Mac OS X Plugin</font></strong></td>
- <td valign="TOP" align="RIGHT">
- <font size="-1">
-- <strong>Version 1.3 </strong>
-- <br/> By Seph M. Soliman and Alan Ezust
-+ <strong>Version 1.4 </strong>
-+ <br/> By Seph M. Soliman, Alan Ezust, Makarius
- <br/> $Date: 2013-09-19 17:42:51 +0000 (Thu, 19 Sep 2013) $
- </font>
- </td>
-diff -ru MacOSX-trunk-r24891/macosx/MacOSXPlugin.java MacOSX-trunk/macosx/MacOSXPlugin.java
---- MacOSX-trunk-r24891/macosx/MacOSXPlugin.java 2013-09-20 02:51:27.000000000 +0200
-+++ MacOSX-trunk/macosx/MacOSXPlugin.java 2019-05-08 17:25:14.905716526 +0200
-@@ -25,6 +25,7 @@
- //{{{ Imports
- import java.awt.event.InputEvent;
-
-+import java.awt.Desktop;
- import javax.swing.*;
- import java.util.regex.Pattern;
- import java.io.File;
-@@ -59,17 +60,13 @@
- {
- try
- {
-- MacOSXPlugin listener = MacOSXPlugin.this;
-- Class theClass = listener.getClass();
--
-- // Generate and register the OSXAdapter, passing it a hash of all the methods we wish to
-- // use as delegates for various com.apple.eawt.ApplicationListener methods
-- OSXAdapter.setQuitHandler(listener, theClass.getDeclaredMethod("handleQuit", (Class[])null));
-- OSXAdapter.setAboutHandler(listener, theClass.getDeclaredMethod("handleAbout", (Class[])null));
-- OSXAdapter.setPreferencesHandler(listener, theClass.getDeclaredMethod("handlePreferences", (Class[])null));
-- OSXAdapter.setFileHandler(listener, theClass.getDeclaredMethod("handleOpenFile", new Class[] { String.class }));
-- OSXAdapter.setReOpenApplicationHandler(listener, theClass.getDeclaredMethod("handleReOpenApplication", (Class[])null));
--
-+ Desktop desktop = Desktop.getDesktop();
-+
-+ desktop.setQuitHandler((e, r) -> { handleQuit(); r.cancelQuit(); });
-+ desktop.setAboutHandler((e) -> handleAbout());
-+ desktop.setPreferencesHandler((e) -> handlePreferences());
-+ desktop.setOpenFileHandler((e) -> { for (File f : e.getFiles()) handleOpenFile(f); });
-+
- String lf = jEdit.getProperty("lookAndFeel");
- if(lf != null && lf.length() != 0)
- {
-@@ -86,7 +83,7 @@
- }
- catch (Exception e)
- {
-- Log.log(Log.ERROR, this, "Error while loading the OSXAdapter:", e);
-+ Log.log(Log.ERROR, this, "Error while configuring MacOSX support:", e);
- }
- }
- };
-@@ -109,7 +106,7 @@
- //JOptionPane.showMessageDialog(null, jEdit.getProperty("MacOSXPlugin.dialog.unload.message"), jEdit.getProperty("MacOSXPlugin.dialog.unload.title"), 1);
- }
-
-- // General quit handler; fed to the OSXAdapter as the method to call when a system quit event occurs
-+ // General quit handler; the method to call when a system quit event occurs
- // A quit event is triggered by Cmd-Q, selecting Quit from the application or Dock menu, or logging out
- public boolean handleQuit()
- {
-@@ -122,16 +119,14 @@
- new CombinedOptions(jEdit.getActiveView());
- }
-
-- // General info dialog; fed to the OSXAdapter as the method to call when
-- // "About OSXAdapter" is selected from the application menu
-+ // General info dialog; the method to call when "About" is selected from the application menu
- public void handleAbout()
- {
- new AboutDialog(jEdit.getActiveView());
- }
-
-- public void handleOpenFile(String filepath)
-+ public void handleOpenFile(File file)
- {
-- File file = new File(filepath);
- if(file.exists())
- {
- if(file.isDirectory())
-@@ -152,7 +147,7 @@
- }
-
- if (jEdit.openFile(view, file.getPath()) == null)
-- Log.log(Log.ERROR, this, "Unable to open file: " + filepath);
-+ Log.log(Log.ERROR, this, "Unable to open file: " + file.getPath());
- }
- else
- {
-@@ -161,7 +156,7 @@
- }
- else
- {
-- Log.log(Log.ERROR, this, "Cannot open non-existing file: " + filepath);
-+ Log.log(Log.ERROR, this, "Cannot open non-existing file: " + file.getPath());
- }
-
- }
-@@ -198,9 +193,6 @@
- {
- ViewUpdate msg = (ViewUpdate)message;
- refreshProxyIcon(msg.getView());
--
-- if (msg.getWhat() == ViewUpdate.CREATED)
-- enableFullScreenMode(msg.getView());
- }
- else if(message instanceof EditPaneUpdate)
- {
-@@ -312,26 +304,6 @@
- return jEdit.getBooleanProperty("plugin.MacOSXPlugin.disableOption");
- }
-
-- public void enableFullScreenMode(View view)
-- {
-- if (fullScreenFailed)
-- return;
--
-- try
-- {
-- // FullScreenUtilities.setWindowCanFullScreen(view, true);
-- Class<?> Util = Class.forName("com.apple.eawt.FullScreenUtilities");
-- Class arguments[] = new Class[] { java.awt.Window.class, Boolean.TYPE };
-- Method setWindowCanFullScreen = Util.getMethod("setWindowCanFullScreen", arguments);
-- setWindowCanFullScreen.invoke(Util, view, true);
-- }
-- catch (Exception e)
-- {
-- Log.log(Log.DEBUG, this, "Unable to enable OS X native full screen mode: " + e);
-- fullScreenFailed = true;
-- }
-- }
--
- //{{{ osok() method
- private boolean osok()
- {
-@@ -344,10 +316,4 @@
-
- return true;
- }//}}}
--
-- //{{{ Instance variables
--
-- // If unable to enable full screen mode (e.g., running on OSX 10.6 or earlier), don't keep trying
-- private boolean fullScreenFailed = false;
-- //}}}
- }
-Only in MacOSX-trunk-r24891/macosx: OSXAdapter.java
-diff -ru MacOSX-trunk-r24891/MacOSX.props MacOSX-trunk/MacOSX.props
---- MacOSX-trunk-r24891/MacOSX.props 2013-09-24 01:12:13.000000000 +0200
-+++ MacOSX-trunk/MacOSX.props 2019-05-08 17:07:07.001576716 +0200
-@@ -5,8 +5,8 @@
- # Plugin info
- #
- plugin.macosx.MacOSXPlugin.name=Mac OS X Support
--plugin.macosx.MacOSXPlugin.author=Seph Soliman, Alan Ezust
--plugin.macosx.MacOSXPlugin.version=1.3
-+plugin.macosx.MacOSXPlugin.author=Seph Soliman, Alan Ezust, Makarius
-+plugin.macosx.MacOSXPlugin.version=1.4
- plugin.macosx.MacOSXPlugin.docs=docs/MacOSX.html
- plugin.macosx.MacOSXPlugin.description=Provides better MacOS X integration through features such as better CMD-key mapping, drag-and-drop from Finder and more.
- plugin.macosx.MacOSXPlugin.longdescription=description.html
-@@ -15,7 +15,7 @@
- # Dependencies
- #
- plugin.macosx.MacOSXPlugin.depend.0=jedit 05.01.99.00
--plugin.macosx.MacOSXPlugin.depend.1=jdk 1.6
-+plugin.macosx.MacOSXPlugin.depend.1=jdk 1.9
-
- MacOSXPlugin.depend.os.name=Mac OS X
- MacOSXPlugin.depend.mrj.version=99
--- a/src/Tools/jEdit/patches/props Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/props Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/jedit/localization/jedit_en.props 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props
---- 5.5.0/jEdit/org/jedit/localization/jedit_en.props 2018-04-09 01:58:42.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props 2019-02-24 12:21:02.506652445 +0100
-@@ -1270,8 +1270,7 @@
+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
+@@ -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\
for a full stack trace.
--- a/src/Tools/jEdit/patches/putenv Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/putenv Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2018-04-09 01:57:06.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2019-02-24 12:21:09.602678130 +0100
-@@ -126,6 +126,21 @@
+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
+@@ -131,6 +131,21 @@
static final Pattern winPattern = Pattern.compile(winPatternString);
@@ -23,7 +23,7 @@
/** A helper function for expandVariables when handling Windows paths on non-windows systems.
*/
private static String win2unix(String winPath)
-@@ -135,7 +150,7 @@
+@@ -140,7 +155,7 @@
if (m.find())
{
String varName = m.group(2);
@@ -32,7 +32,7 @@
if (expansion != null)
return m.replaceFirst(expansion);
}
-@@ -174,7 +189,7 @@
+@@ -179,7 +194,7 @@
return arg;
}
String varName = m.group(2);
@@ -41,7 +41,7 @@
if (expansion == null) {
if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
expansion = jEdit.getSettingsDirectory();
-@@ -184,7 +199,7 @@
+@@ -189,7 +204,7 @@
varName = varName.toUpperCase();
String uparg = arg.toUpperCase();
m = p.matcher(uparg);
@@ -50,7 +50,7 @@
}
}
if (expansion != null) {
-@@ -1637,13 +1652,11 @@
+@@ -1682,13 +1697,11 @@
//{{{ VarCompressor constructor
VarCompressor()
{
--- a/src/Tools/jEdit/patches/title Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/title Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/View.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/View.java 2018-04-09 01:57:31.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/View.java 2019-02-24 12:21:17.050704937 +0100
-@@ -1233,15 +1233,10 @@
+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
+@@ -1262,15 +1262,10 @@
StringBuilder title = new StringBuilder();
--- a/src/Tools/jEdit/patches/vfs_manager Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/vfs_manager Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2018-04-09 01:57:13.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2019-02-24 12:21:25.986736893 +0100
-@@ -345,6 +345,18 @@
+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
+@@ -380,6 +380,18 @@
if(vfsUpdates.size() == 1)
{
--- a/src/Tools/jEdit/patches/vfs_marker Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/vfs_marker Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2018-04-09 01:57:42.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2019-02-24 12:23:42.403199825 +0100
-@@ -1204,6 +1204,7 @@
+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
+@@ -1194,6 +1194,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
Buffer buffer = null;
@@ -9,7 +9,7 @@
check_selected:
for (VFSFile file : selectedFiles)
-@@ -1253,7 +1254,10 @@
+@@ -1243,7 +1244,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)
-@@ -1262,21 +1266,30 @@
+@@ -1252,21 +1256,30 @@
if(buffer != null)
{
@@ -53,10 +53,10 @@
}
Object[] listeners = listenerList.getListenerList();
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2018-04-09 01:57:13.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2019-02-24 12:23:42.403199825 +0100
-@@ -297,6 +297,12 @@
+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
+@@ -302,6 +302,12 @@
}
} //}}}
@@ -69,10 +69,10 @@
//{{{ getPath() method
public String getPath()
{
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java 2018-04-09 01:56:22.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2019-02-24 12:23:42.403199825 +0100
-@@ -4479,7 +4479,7 @@
+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
+@@ -4242,7 +4242,7 @@
} //}}}
//{{{ gotoMarker() method
--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Jun 10 19:59:12 2020 +0200
@@ -396,7 +396,12 @@
x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
{
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
- val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
+ val chunk_str =
+ if (chunk.chars == null) Symbol.spaces(chunk.length)
+ else {
+ if (chunk.str == null) { chunk.str = new String(chunk.chars) }
+ chunk.str
+ }
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor