--- 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
--- 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
--- 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 <<EOF
Original jEdit Documentation
- jedit-manual jEdit 5.2 User's Guide
- jedit-changes jEdit 5.2 Version History
+ jedit-manual jEdit 5.3 User's Guide
+ jedit-changes jEdit 5.3 Version History
EOF
--- a/src/Tools/jEdit/patches/brackets Fri Oct 23 18:39:14 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-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
-@@ -1613,8 +1618,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.2.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.2.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
---- 5.2.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2015-02-02 02:14:26.000000000 +0100
-+++ 5.2.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2015-02-28 20:53:50.167805688 +0100
-@@ -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';
- }
- } //}}}
--- /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(){}
+ }
--- 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)}
--- 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();
- } //}}}
-
--- 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.
--- /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;
+ }
+ }
+
--- 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);
--- 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
--- 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<Object> keys() {
-+ return Collections.enumeration(new TreeSet<Object>(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)
- {
--- 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);
- }
- }
-
--- 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