# HG changeset patch # User wenzelm # Date 1591811952 -7200 # Node ID 65fd0f032a75c19d9da0389ec165315cb32614b6 # Parent 0c8a9c02830413a0c0d20bdfebb223eaa30fc355 updated to jedit-5.6pre1 (repository version 25349); diff -r 0c8a9c028304 -r 65fd0f032a75 Admin/components/components.sha1 --- 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 diff -r 0c8a9c028304 -r 65fd0f032a75 Admin/components/main --- 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 diff -r 0c8a9c028304 -r 65fd0f032a75 NEWS --- 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 diff -r 0c8a9c028304 -r 65fd0f032a75 src/Pure/Admin/build_release.scala --- 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 diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/lib/Tools/jedit --- 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" <jEdit Mac OS X Plugin - - -- Version 1.3 --
By Seph M. Soliman and Alan Ezust -+ Version 1.4 -+
By Seph M. Soliman, Alan Ezust, Makarius -
$Date: 2013-09-19 17:42:51 +0000 (Thu, 19 Sep 2013) $ - - -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 diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/patches/props --- 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. diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/patches/putenv --- 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() { diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/patches/title --- 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(); diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/patches/vfs_manager --- 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) { diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/patches/vfs_marker --- 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 diff -r 0c8a9c028304 -r 65fd0f032a75 src/Tools/jEdit/src/rich_text_area.scala --- 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