# HG changeset patch # User wenzelm # Date 1445626996 -7200 # Node ID d40f906bb13f35d3e4746c149f48ed96bc1d2c65 # Parent 9f7453fb022fb4151b28329e7097e05ef99cb50e updated to jedit-5.3.0 and SideKick 1.8; diff -r 9f7453fb022f -r d40f906bb13f Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Oct 23 18:39:14 2015 +0200 +++ b/Admin/components/components.sha1 Fri Oct 23 21:03:16 2015 +0200 @@ -74,6 +74,7 @@ d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz 14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz +b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz diff -r 9f7453fb022f -r d40f906bb13f Admin/components/main --- a/Admin/components/main Fri Oct 23 18:39:14 2015 +0200 +++ b/Admin/components/main Fri Oct 23 21:03:16 2015 +0200 @@ -6,7 +6,7 @@ Haskabelle-2015 isabelle_fonts-20151021 jdk-8u66 -jedit_build-20150228 +jedit_build-20151023 jfreechart-1.0.14-1 jortho-1.0-2 kodkodi-1.5.2 diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Oct 23 18:39:14 2015 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Oct 23 21:03:16 2015 +0200 @@ -341,12 +341,12 @@ cd ../.. rm -rf dist/classes - cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.2.0manual-a4.pdf" dist/doc/jedit-manual.pdf + cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf cp dist/doc/CHANGES.txt dist/doc/jedit-changes cat > dist/doc/Contents <'; - 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 -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/brackets_extended_styles --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/brackets_extended_styles Fri Oct 23 21:03:16 2015 +0200 @@ -0,0 +1,142 @@ +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/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java +--- 5.3.0/jEdit/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-10-23 20:02:22.161225360 +0200 +@@ -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,9 @@ + Log.log(Log.ERROR,StandardUtilities.class,e); + } + } +- +- return styles; ++ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); ++ return _styleExtender.extendStyles(styles); + } //}}} +- ++ + private SyntaxUtilities(){} + } diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/content_margin --- a/src/Tools/jEdit/patches/content_margin Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2015-02-02 02:14:27.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2015-02-28 20:54:24.803916543 +0100 -@@ -95,6 +95,7 @@ - closeBox.putClientProperty("JButton.buttonType","toolbar"); - - closeBox.setMargin(new Insets(0,0,0,0)); -+ GUIUtilities.setButtonContentMargin(closeBox, closeBox.getMargin()); - - closeBox.addActionListener(new ActionHandler()); - -@@ -105,6 +106,7 @@ - menuBtn.putClientProperty("JButton.buttonType","toolbar"); - - menuBtn.setMargin(new Insets(0,0,0,0)); -+ GUIUtilities.setButtonContentMargin(menuBtn, menuBtn.getMargin()); - - menuBtn.addMouseListener(new MenuMouseHandler()); - -@@ -148,6 +150,7 @@ - - JToggleButton button = new JToggleButton(); - button.setMargin(new Insets(1,1,1,1)); -+ GUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6)); - button.setRequestFocusEnabled(false); - button.setIcon(new RotatedTextIcon(rotation,button.getFont(), - entry.shortTitle())); -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2015-02-02 02:14:29.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2015-02-28 20:54:24.803916543 +0100 -@@ -38,6 +38,7 @@ - import org.gjt.sp.jedit.textarea.TextAreaMouseHandler; - import org.gjt.sp.util.Log; - import org.gjt.sp.util.SyntaxUtilities; -+import javax.swing.UIDefaults; - - - import java.net.URL; -@@ -1834,6 +1835,21 @@ - return (View)getComponentParent(comp,View.class); - } //}}} - -+ //{{{ setButtonContentMargin() method -+ /** -+ * Sets the content margin of a button (for Nimbus L&F). -+ * @param button the button to modify -+ * @param margin the new margin -+ * @since jEdit 5.3 -+ */ -+ public static void setButtonContentMargin(AbstractButton button, Insets margin) -+ { -+ UIDefaults defaults = new UIDefaults(); -+ defaults.put("Button.contentMargins", margin); -+ defaults.put("ToggleButton.contentMargins", margin); -+ button.putClientProperty("Nimbus.Overrides", defaults); -+ } //}}} -+ - //{{{ addSizeSaver() method - /** - * Adds a SizeSaver to the specified Frame. For non-Frame's use {@link #saveGeometry(Window,String)} diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/docking --- a/src/Tools/jEdit/patches/docking Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2015-02-02 02:14:28.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2015-02-28 20:55:01.800035337 +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; -@@ -50,7 +50,7 @@ - * @version $Id: FloatingWindowContainer.java 21831 2012-06-18 22:54:17Z ezust $ - * @since jEdit 4.0pre1 - */ --public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, -+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, - PropertyChangeListener - { - String dockableName = null; -@@ -58,6 +58,8 @@ - public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager, - boolean clone) - { -+ super(dockableWindowManager.getView()); -+ - this.dockableWindowManager = dockableWindowManager; - - dockableWindowManager.addPropertyChangeListener(this); -@@ -93,7 +95,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); -@@ -160,8 +161,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(); - } //}}} - diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/extended_styles --- a/src/Tools/jEdit/patches/extended_styles Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2015-02-02 02:14:28.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2015-02-28 20:55:21.136097582 +0100 -@@ -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.2.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2015-02-02 02:14:29.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2015-02-28 20:55:21.136097582 +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.2.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2015-02-02 02:14:29.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2015-02-28 20:55:21.140097595 +0100 -@@ -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.2.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.2.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java ---- 5.2.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2015-02-02 02:14:30.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-02-28 20:55:21.140097595 +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,9 @@ - Log.log(Log.ERROR,StandardUtilities.class,e); - } - } -- -- return styles; -+ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size)); -+ return _styleExtender.extendStyles(styles); - } //}}} -- -+ - private SyntaxUtilities(){} - } -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2015-02-02 02:14:27.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2015-02-28 20:55:21.140097595 +0100 -@@ -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. diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/file_completion --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/file_completion Fri Oct 23 21:03:16 2015 +0200 @@ -0,0 +1,21 @@ +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; + } + } + diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/folding --- a/src/Tools/jEdit/patches/folding Fri Oct 23 18:39:14 2015 +0200 +++ b/src/Tools/jEdit/patches/folding Fri Oct 23 21:03:16 2015 +0200 @@ -1,7 +1,7 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-02-02 02:14:26.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-02-28 20:55:39.932158194 +0100 -@@ -1936,29 +1936,23 @@ +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 @@ { Segment seg = new Segment(); newFoldLevel = foldHandler.getFoldLevel(this,i,seg); diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/numeric_keypad --- a/src/Tools/jEdit/patches/numeric_keypad Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2015-02-02 02:14:28.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2015-02-28 20:56:06.676244609 +0100 -@@ -129,7 +129,7 @@ - case KeyEvent.VK_OPEN_BRACKET : - case KeyEvent.VK_BACK_SLASH : - case KeyEvent.VK_CLOSE_BRACKET: -- /* case KeyEvent.VK_NUMPAD0 : -+ case KeyEvent.VK_NUMPAD0 : - case KeyEvent.VK_NUMPAD1 : - case KeyEvent.VK_NUMPAD2 : - case KeyEvent.VK_NUMPAD3 : -@@ -144,7 +144,7 @@ - case KeyEvent.VK_SEPARATOR: - case KeyEvent.VK_SUBTRACT : - case KeyEvent.VK_DECIMAL : -- case KeyEvent.VK_DIVIDE :*/ -+ case KeyEvent.VK_DIVIDE : - case KeyEvent.VK_BACK_QUOTE: - case KeyEvent.VK_QUOTE: - case KeyEvent.VK_DEAD_GRAVE: -@@ -191,28 +191,7 @@ - //{{{ isNumericKeypad() method - public static boolean isNumericKeypad(int keyCode) - { -- switch(keyCode) -- { -- case KeyEvent.VK_NUMPAD0: -- case KeyEvent.VK_NUMPAD1: -- case KeyEvent.VK_NUMPAD2: -- case KeyEvent.VK_NUMPAD3: -- case KeyEvent.VK_NUMPAD4: -- case KeyEvent.VK_NUMPAD5: -- case KeyEvent.VK_NUMPAD6: -- case KeyEvent.VK_NUMPAD7: -- case KeyEvent.VK_NUMPAD8: -- case KeyEvent.VK_NUMPAD9: -- case KeyEvent.VK_MULTIPLY: -- case KeyEvent.VK_ADD: -- /* case KeyEvent.VK_SEPARATOR: */ -- case KeyEvent.VK_SUBTRACT: -- case KeyEvent.VK_DECIMAL: -- case KeyEvent.VK_DIVIDE: -- return true; -- default: -- return false; -- } -+ return false; - } //}}} - - //{{{ processKeyEvent() method diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/sorted_properties --- a/src/Tools/jEdit/patches/sorted_properties Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2015-02-02 02:14:29.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2015-02-28 20:56:21.612292958 +0100 -@@ -1505,6 +1505,27 @@ - - //}}} - -+ //{{{ storeProperties() method -+ /** -+ * Stores properties with sorted keys. -+ * @param props Given properties. -+ * @param out Output stream. -+ * @param comments Description of the property list. -+ * @since jEdit 5.3 -+ */ -+ public static void storeProperties(Properties props, OutputStream out, String comments) -+ throws IOException -+ { -+ Properties sorted = new Properties() { -+ @Override -+ public synchronized Enumeration keys() { -+ return Collections.enumeration(new TreeSet(super.keySet())); -+ } -+ }; -+ sorted.putAll(props); -+ sorted.store(out, comments); -+ } //}}} -+ - static VarCompressor svc = null; - - //{{{ VarCompressor class -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 2015-02-02 02:14:29.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java 2015-02-28 20:56:21.612292958 +0100 -@@ -77,7 +77,7 @@ - void saveUserProps(OutputStream out) - throws IOException - { -- user.store(out,"jEdit properties"); -+ MiscUtilities.storeProperties(user, out, "jEdit properties"); - } //}}} - - //{{{ loadPluginProps() method -diff -ru 5.2.0/jEdit/org/jedit/keymap/KeymapImpl.java 5.2.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java ---- 5.2.0/jEdit/org/jedit/keymap/KeymapImpl.java 2015-02-02 02:14:25.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java 2015-02-28 20:56:21.612292958 +0100 -@@ -32,6 +32,7 @@ - import java.io.InputStream; - import java.util.Properties; - -+import org.gjt.sp.jedit.MiscUtilities; - import org.gjt.sp.util.IOUtilities; - import org.gjt.sp.util.Log; - //}}} -@@ -150,7 +151,7 @@ - try - { - out = new BufferedOutputStream(new FileOutputStream(userKeymapFile)); -- props.store(out, "jEdit's keymap " + name); -+ MiscUtilities.storeProperties(props, out, "jEdit's keymap " + name); - } - catch (IOException e) - { diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/patches/structure_matcher --- a/src/Tools/jEdit/patches/structure_matcher Fri Oct 23 18:39:14 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -diff -ru 5.2.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java ---- 5.2.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 2015-02-02 02:14:27.000000000 +0100 -+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java 2015-02-28 20:56:32.644328711 +0100 -@@ -201,8 +201,9 @@ - int matchEndLine = textArea.getScreenLineOfOffset( - match.end); - -- int fontHeight = textArea.getPainter().getFontHeight(); -- y += textArea.getPainter().getLineExtraSpacing(); -+ int height = Math.min( -+ textArea.getPainter().getLineHeight(), textArea.getPainter().getFontHeight()); -+ y += Math.max(textArea.getPainter().getLineExtraSpacing(), 0); - - int[] offsets = getOffsets(screenLine,match); - int x1 = offsets[0]; -@@ -210,8 +211,8 @@ - - gfx.setColor(textArea.getPainter().getStructureHighlightColor()); - -- gfx.drawLine(x1,y,x1,y + fontHeight - 1); -- gfx.drawLine(x2,y,x2,y + fontHeight - 1); -+ gfx.drawLine(x1,y,x1,y + height - 1); -+ gfx.drawLine(x2,y,x2,y + height - 1); - - if(matchStartLine == screenLine || screenLine == 0) - gfx.drawLine(x1,y,x2,y); -@@ -229,8 +230,8 @@ - - if(matchEndLine == screenLine) - { -- gfx.drawLine(x1,y + fontHeight - 1, -- x2,y + fontHeight - 1); -+ gfx.drawLine(x1,y + height - 1, -+ x2,y + height - 1); - } - } - diff -r 9f7453fb022f -r d40f906bb13f src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Fri Oct 23 18:39:14 2015 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Fri Oct 23 21:03:16 2015 +0200 @@ -14,10 +14,10 @@ #dependencies plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7 -plugin.isabelle.jedit.Plugin.depend.1=jedit 05.02.00.00 +plugin.isabelle.jedit.Plugin.depend.1=jedit 05.03.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.7 +plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8 plugin.isabelle.jedit.Plugin.depend.5=plugin gatchan.highlight.HighlightPlugin 2.0 #options