--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/brackets Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,26 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +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';
+ }
+ } //}}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/extended_styles Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,105 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2013-07-28 19:03:38.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2013-09-05 10:51:29.192192327 +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.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2013-07-28 19:03:51.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2013-09-05 10:51:29.192192327 +0200
+@@ -256,9 +256,9 @@
+ //{{{ Package private members
+
+ //{{{ Instance variables
+- SyntaxStyle style;
++ public SyntaxStyle style;
+ // set up after init()
+- float width;
++ public float width;
+ //}}}
+
+ //{{{ Chunk constructor
+@@ -506,7 +506,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.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2013-07-28 19:03:51.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2013-09-05 10:51:29.192192327 +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.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2013-07-28 19:03:53.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2013-09-05 10:51:29.192192327 +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 -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-05 10:51:29.196192309 +0200
+@@ -907,6 +907,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.
--- a/src/Tools/jEdit/patches/jedit/brackets Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +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';
- }
- } //}}}
--- a/src/Tools/jEdit/patches/jedit/extended_styles Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2013-07-28 19:03:38.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2013-09-05 10:51:29.192192327 +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.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2013-07-28 19:03:51.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2013-09-05 10:51:29.192192327 +0200
-@@ -256,9 +256,9 @@
- //{{{ Package private members
-
- //{{{ Instance variables
-- SyntaxStyle style;
-+ public SyntaxStyle style;
- // set up after init()
-- float width;
-+ public float width;
- //}}}
-
- //{{{ Chunk constructor
-@@ -506,7 +506,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.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2013-07-28 19:03:51.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2013-09-05 10:51:29.192192327 +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.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2013-07-28 19:03:53.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2013-09-05 10:51:29.192192327 +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 -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-05 10:51:29.196192309 +0200
-@@ -907,6 +907,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.
--- a/src/Tools/jEdit/patches/jedit/macos Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 2013-07-28 19:03:49.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-09-05 10:55:36.388181955 +0200
-@@ -109,7 +109,7 @@
- * used to handle a modifier key press in conjunction with an alphabet
- * key. <b>On by default on MacOS.</b>
- */
-- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
-+ public static boolean ALTERNATIVE_DISPATCHER = false;
-
- /**
- * If true, A+ shortcuts are disabled. If you use this, you should also
-
--- a/src/Tools/jEdit/patches/jedit/numeric_keypad Wed Sep 25 20:28:49 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
---- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-07-28 19:03:38.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-09-10 21:55:21.220043663 +0200
-@@ -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:
-@@ -202,28 +202,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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/macos Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,13 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 2013-07-28 19:03:49.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-09-05 10:55:36.388181955 +0200
+@@ -109,7 +109,7 @@
+ * used to handle a modifier key press in conjunction with an alphabet
+ * key. <b>On by default on MacOS.</b>
+ */
+- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
++ public static boolean ALTERNATIVE_DISPATCHER = false;
+
+ /**
+ * If true, A+ shortcuts are disabled. If you use this, you should also
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/numeric_keypad Wed Sep 25 20:29:28 2013 +0200
@@ -0,0 +1,50 @@
+--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-07-28 19:03:38.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-09-10 21:55:21.220043663 +0200
+@@ -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:
+@@ -202,28 +202,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