updated to jedit-5.2.0;
updated CommonControls.jar, kappalayout.jar, MacOSX.jar, SideKick.jar;
--- a/Admin/components/components.sha1 Sat Feb 28 08:50:00 2015 +0100
+++ b/Admin/components/components.sha1 Sat Feb 28 21:51:34 2015 +0100
@@ -65,6 +65,7 @@
f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz
d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz
f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz
+14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.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 Sat Feb 28 08:50:00 2015 +0100
+++ b/Admin/components/main Sat Feb 28 21:51:34 2015 +0100
@@ -5,7 +5,7 @@
exec_process-1.0.3
Haskabelle-2014
jdk-7u76
-jedit_build-20141104
+jedit_build-20150228
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Feb 28 21:51:34 2015 +0100
@@ -327,12 +327,12 @@
cd ../..
rm -rf dist/classes
- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.1.0manual-a4.pdf" dist/doc/jedit-manual.pdf
+ cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.2.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.1 User's Guide
- jedit-changes jEdit 5.1 Version History
+ jedit-manual jEdit 5.2 User's Guide
+ jedit-changes jEdit 5.2 Version History
EOF
--- a/src/Tools/jEdit/patches/brackets Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/brackets Sat Feb 28 21:51:34 2015 +0100
@@ -1,7 +1,7 @@
-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-26 16:09:50.131780476 +0200
-@@ -1610,8 +1615,8 @@
+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
@@ -12,9 +12,9 @@
int count = 1;
char openBracket = '\0';
char closeBracket = '\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
+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 '>';
--- a/src/Tools/jEdit/patches/content_margin Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/content_margin Sat Feb 28 21:51:34 2015 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2013-07-28 19:03:36.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2014-11-04 17:51:00.000000000 +0100
+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");
@@ -25,9 +25,9 @@
button.setRequestFocusEnabled(false);
button.setIcon(new RotatedTextIcon(rotation,button.getFont(),
entry.shortTitle()));
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2013-07-28 19:03:53.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2014-11-04 17:52:52.000000000 +0100
+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;
@@ -36,7 +36,7 @@
import java.net.URL;
-@@ -1833,6 +1834,21 @@
+@@ -1834,6 +1835,21 @@
return (View)getComponentParent(comp,View.class);
} //}}}
@@ -58,4 +58,3 @@
//{{{ addSizeSaver() method
/**
* Adds a SizeSaver to the specified Frame. For non-Frame's use {@link #saveGeometry(Window,String)}
-
--- a/src/Tools/jEdit/patches/docking Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/docking Sat Feb 28 21:51:34 2015 +0100
@@ -1,18 +1,6 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java
---- jEdit/org/gjt/sp/jedit/gui/DockableWindowContainer.java 2013-07-28 19:03:36.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/DockableWindowContainer.java 2014-05-11 19:41:50.786012120 +0200
-@@ -26,7 +26,7 @@
- * @version $Id: DockableWindowContainer.java 21502 2012-03-29 17:19:44Z ezust $
- * @since jEdit 2.6pre3
- */
--interface DockableWindowContainer
-+public interface DockableWindowContainer
- {
- void register(DockableWindowManagerImpl.Entry entry);
- void remove(DockableWindowManagerImpl.Entry entry);
-diff -ru jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2013-07-28 19:03:38.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2014-05-11 19:32:49.710039809 +0200
+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;
--- a/src/Tools/jEdit/patches/extended_styles Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/extended_styles Sat Feb 28 21:51:34 2015 +0100
@@ -1,6 +1,6 @@
-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
+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;
@@ -10,10 +10,10 @@
{
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 @@
+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
@@ -25,7 +25,7 @@
//}}}
//{{{ Chunk constructor
-@@ -506,7 +506,7 @@
+@@ -509,7 +509,7 @@
// this is either style.getBackgroundColor() or
// styles[defaultID].getBackgroundColor()
private Color background;
@@ -34,9 +34,9 @@
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
+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)
@@ -46,9 +46,9 @@
} //}}}
//{{{ 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
+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);
@@ -88,10 +88,10 @@
+
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 @@
+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;
} //}}}
--- a/src/Tools/jEdit/patches/folding Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/folding Sat Feb 28 21:51:34 2015 +0100
@@ -1,7 +1,7 @@
-diff -ru jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2013-07-28 19:03:27.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2014-10-18 21:35:15.946285279 +0200
-@@ -1945,29 +1945,23 @@
+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 @@
{
Segment seg = new Segment();
newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
--- a/src/Tools/jEdit/patches/macos Sat Feb 28 08:50:00 2015 +0100
+++ /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/numeric_keypad Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/numeric_keypad Sat Feb 28 21:51:34 2015 +0100
@@ -1,5 +1,6 @@
---- 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
+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 :
@@ -18,7 +19,7 @@
case KeyEvent.VK_BACK_QUOTE:
case KeyEvent.VK_QUOTE:
case KeyEvent.VK_DEAD_GRAVE:
-@@ -202,28 +202,7 @@
+@@ -191,28 +191,7 @@
//{{{ isNumericKeypad() method
public static boolean isNumericKeypad(int keyCode)
{
--- a/src/Tools/jEdit/patches/sorted_properties Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/sorted_properties Sat Feb 28 21:51:34 2015 +0100
@@ -1,7 +1,7 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2013-07-28 19:03:53.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2014-11-04 17:48:25.000000000 +0100
-@@ -1468,6 +1468,27 @@
+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 @@
//}}}
@@ -29,9 +29,9 @@
static VarCompressor svc = null;
//{{{ VarCompressor class
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/PropertyManager.java 2013-07-28 19:03:53.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/PropertyManager.java 2014-11-04 17:45:54.000000000 +0100
+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
@@ -41,9 +41,9 @@
} //}}}
//{{{ loadPluginProps() method
-diff -ru 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java
---- 5.1.0/jEdit/org/jedit/keymap/KeymapImpl.java 2013-07-28 19:03:20.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/jedit/keymap/KeymapImpl.java 2014-11-04 17:58:09.660507580 +0100
+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;
--- a/src/Tools/jEdit/patches/structure_matcher Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/patches/structure_matcher Sat Feb 28 21:51:34 2015 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java
---- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/StructureMatcher.java 2013-07-28 19:03:31.000000000 +0200
-+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/StructureMatcher.java 2014-10-26 15:23:15.176502388 +0100
+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);
--- a/src/Tools/jEdit/src/jedit_lib.scala Sat Feb 28 08:50:00 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Feb 28 21:51:34 2015 +0100
@@ -363,7 +363,7 @@
def special_key(evt: KeyEvent): Boolean =
{
- // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
+ // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
val mod = evt.getModifiers
(mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
(mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&