--- a/Admin/components/components.sha1 Sun Mar 19 18:28:32 2017 +0100
+++ b/Admin/components/components.sha1 Sun Mar 19 20:28:21 2017 +0100
@@ -106,6 +106,7 @@
8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz
c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz
d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz
+d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
--- a/Admin/components/main Sun Mar 19 18:28:32 2017 +0100
+++ b/Admin/components/main Sun Mar 19 20:28:21 2017 +0100
@@ -5,7 +5,7 @@
e-1.8
isabelle_fonts-20160830
jdk-8u121
-jedit_build-20161024
+jedit_build-20170319
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- a/NEWS Sun Mar 19 18:28:32 2017 +0100
+++ b/NEWS Sun Mar 19 20:28:21 2017 +0100
@@ -45,6 +45,8 @@
the document model to theories that are required for open editor
buffers.
+* Update to jedit-5.4.0.
+
*** HOL ***
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Mar 19 18:28:32 2017 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Mar 19 20:28:21 2017 +0100
@@ -353,12 +353,12 @@
cd ../..
rm -rf dist/classes
- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf
+ cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf
cp dist/doc/CHANGES.txt dist/doc/jedit-changes
cat > dist/doc/Contents <<EOF
Original jEdit Documentation
- jedit-manual jEdit 5.3 User's Guide
- jedit-changes jEdit 5.3 Version History
+ jedit-manual jEdit 5.4 User's Guide
+ jedit-changes jEdit 5.4 Version History
EOF
--- a/src/Tools/jEdit/patches/brackets_extended_styles Sun Mar 19 18:28:32 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,144 +0,0 @@
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-20 19:56:05.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2015-10-23 20:02:22.161225360 +0200
-@@ -79,7 +79,7 @@
- start = next;
- token = token.next;
- }
-- if (token.id == Token.END || token.id == Token.NULL)
-+ if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
- {
- JOptionPane.showMessageDialog(textArea.getView(),
- jEdit.getProperty("syntax-style-no-token.message"),
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-20 19:56:07.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2015-10-23 20:02:22.161225360 +0200
-@@ -259,9 +259,9 @@
- //{{{ Package private members
-
- //{{{ Instance variables
-- SyntaxStyle style;
-+ public SyntaxStyle style;
- // set up after init()
-- float width;
-+ public float width;
- //}}}
-
- //{{{ Chunk constructor
-@@ -509,7 +509,7 @@
- // this is either style.getBackgroundColor() or
- // styles[defaultID].getBackgroundColor()
- private Color background;
-- private String str;
-+ public String str;
- private GlyphVector[] glyphs;
- //}}}
-
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2015-10-20 19:56:07.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2015-10-23 20:02:22.161225360 +0200
-@@ -57,7 +57,7 @@
- */
- public static String tokenToString(byte token)
- {
-- return (token == Token.END) ? "END" : TOKEN_TYPES[token];
-+ return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
- } //}}}
-
- //{{{ Token types
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-20 19:56:03.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2015-10-23 20:02:22.161225360 +0200
-@@ -910,6 +910,11 @@
- return chunkCache.getLineInfo(screenLine).physicalLine;
- } //}}}
-
-+ public Chunk getChunksOfScreenLine(int screenLine)
-+ {
-+ return chunkCache.getLineInfo(screenLine).chunks;
-+ }
-+
- //{{{ getScreenLineOfOffset() method
- /**
- * Returns the screen (wrapped) line containing the specified offset.
-@@ -1618,8 +1623,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.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2015-10-20 19:56:00.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2015-10-23 19:46:33.728522904 +0200
-@@ -97,6 +97,22 @@
- 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 '«';
-+ 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 '⟨';
-+ 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 '⌊';
-+ 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 '⟦';
-+ case '⦃': if (direction != null) direction[0] = true; return '⦄';
-+ case '⦄': if (direction != null) direction[0] = false; return '⦃';
- default: return '\0';
- }
- } //}}}
-diff -ru 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-11-24 22:14:56.935661997 +0100
-@@ -194,7 +194,24 @@
- {
- return loadStyles(family,size,true);
- }
--
-+
-+ /**
-+ * Extended styles derived from the user-specified style array.
-+ */
-+
-+ public static class StyleExtender
-+ {
-+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
-+ {
-+ return styles;
-+ }
-+ }
-+ volatile private static StyleExtender _styleExtender = new StyleExtender();
-+ public static void setStyleExtender(StyleExtender ext)
-+ {
-+ _styleExtender = ext;
-+ }
-+
- /**
- * Loads the syntax styles from the properties, giving them the specified
- * base font family and size.
-@@ -224,9 +241,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(){}
- }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/docking Sun Mar 19 20:28:21 2017 +0100
@@ -0,0 +1,52 @@
+diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2017-03-18 14:30:25.000000000 +0100
++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2017-03-19 19:27:45.730945687 +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 $
+ * @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 FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
+ boolean clone)
+ {
++ super(dockableWindowManager.getView());
++
+ this.dockableWindowManager = dockableWindowManager;
+
+ dockableWindowManager.addPropertyChangeListener(this);
+@@ -94,7 +96,6 @@
+ pack();
+ Container parent = dockableWindowManager.getView();
+ GUIUtilities.loadGeometry(this, parent, dockableName);
+- GUIUtilities.addSizeSaver(this, parent, dockableName);
+ KeyListener listener = dockableWindowManager.closeListener(dockableName);
+ addKeyListener(listener);
+ getContentPane().addKeyListener(listener);
+@@ -161,8 +162,11 @@
+ @Override
+ public void dispose()
+ {
+- entry.container = null;
+- entry.win = null;
++ GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
++ if (entry != null) {
++ entry.container = null;
++ entry.win = null;
++ }
+ super.dispose();
+ } //}}}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/extended_styles Sun Mar 19 20:28:21 2017 +0100
@@ -0,0 +1,84 @@
+diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-18 14:30:28.000000000 +0100
++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-19 19:27:45.730945687 +0100
+@@ -259,9 +259,9 @@
+ //{{{ Package private members
+
+ //{{{ Instance variables
+- SyntaxStyle style;
++ public SyntaxStyle style;
+ // set up after init()
+- float width;
++ public float width;
+ //}}}
+
+ //{{{ Chunk constructor
+@@ -509,7 +509,7 @@
+ // this is either style.getBackgroundColor() or
+ // styles[defaultID].getBackgroundColor()
+ private Color background;
+- private String str;
++ public String str;
+ private GlyphVector[] glyphs;
+ //}}}
+
+diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-18 14:30:28.000000000 +0100
++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-19 19:27:45.734945702 +0100
+@@ -917,6 +917,11 @@
+ return chunkCache.getLineInfo(screenLine).physicalLine;
+ } //}}}
+
++ public Chunk getChunksOfScreenLine(int screenLine)
++ {
++ return chunkCache.getLineInfo(screenLine).chunks;
++ }
++
+ //{{{ getScreenLineOfOffset() method
+ /**
+ * Returns the screen (wrapped) line containing the specified offset.
+Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig
+diff -ru 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2017-03-18 14:30:34.000000000 +0100
++++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2017-03-19 19:27:45.734945702 +0100
+@@ -200,7 +200,24 @@
+ {
+ return loadStyles(family,size,true);
+ }
+-
++
++ /**
++ * Extended styles derived from the user-specified style array.
++ */
++
++ public static class StyleExtender
++ {
++ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
++ {
++ return styles;
++ }
++ }
++ volatile private static StyleExtender _styleExtender = new StyleExtender();
++ public static void setStyleExtender(StyleExtender ext)
++ {
++ _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/file_completion Sun Mar 19 18:28:32 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2015-10-20 19:56:08.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2015-10-23 20:06:27.874803025 +0200
-@@ -82,16 +82,7 @@
- }
- else if(matchAgainst.regionMatches(true,0,str,0,strLen))
- {
-- /* Keep the first match with exact length but different case.
-- * If the first match is not same length, prefer longest match */
-- if(iPotentialMatch == -1
-- || (potentialMatchGTStr
-- && (matchAgainst.length() > potentialMatchLen)))
-- {
-- potentialMatchLen = matchAgainst.length();
-- iPotentialMatch = i;
-- potentialMatchGTStr = potentialMatchLen > strLen;
-- }
-+ return i;
- }
- }
-
--- a/src/Tools/jEdit/patches/folding Sun Mar 19 18:28:32 2017 +0100
+++ b/src/Tools/jEdit/patches/folding Sun Mar 19 20:28:21 2017 +0100
@@ -1,7 +1,7 @@
-diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-20 19:56:02.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-23 20:02:38.897330618 +0200
-@@ -1956,29 +1956,23 @@
+diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2017-03-18 14:30:28.000000000 +0100
++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2017-03-19 19:27:45.734945702 +0100
+@@ -1950,29 +1950,23 @@
{
Segment seg = new Segment();
newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
--- a/src/Tools/jEdit/patches/gutter Sun Mar 19 18:28:32 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-diff -ru 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java
---- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200
-+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100
-@@ -185,8 +185,6 @@
- }
-
- int y = clip.y - clip.y % lineHeight;
-- if (y == 0)
-- y = textArea.getPainter().getLineExtraSpacing();
-
- extensionMgr.paintScreenLineRange(textArea,gfx,
- firstLine,lastLine,y,lineHeight);
-@@ -725,7 +723,7 @@
-
- FontMetrics textAreaFm = textArea.getPainter().getFontMetrics();
- int lineHeight = textArea.getPainter().getLineHeight();
-- int baseline = textAreaFm.getAscent();
-+ int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent();
-
- ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line);
- int physicalLine = info.physicalLine;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/props Sun Mar 19 20:28:21 2017 +0100
@@ -0,0 +1,13 @@
+diff -ru 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props
+--- 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props 2017-03-18 14:30:24.000000000 +0100
++++ 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props 2017-03-19 19:35:49.728895954 +0100
+@@ -1262,8 +1262,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.
+-plugin-error.start-error=Cannot start: {0}\n\
+- Try updating to a newer version of the plugin.
++plugin-error.start-error=Cannot start: {0}
+ 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}.
--- a/src/Tools/jEdit/src/Isabelle.props Sun Mar 19 18:28:32 2017 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Sun Mar 19 20:28:21 2017 +0100
@@ -14,7 +14,7 @@
#dependencies
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
-plugin.isabelle.jedit.Plugin.depend.1=jedit 05.03.00.00
+plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
--- a/src/Tools/jEdit/src/plugin.scala Sun Mar 19 18:28:32 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Mar 19 20:28:21 2017 +0100
@@ -412,17 +412,11 @@
/* strict initialization */
- // adhoc patch of confusing message
- val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
- jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}")
-
init_options()
init_resources()
init_session()
PIDE._plugin = this
- jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
-
/* non-strict initialization */