1.1 --- a/Admin/components/components.sha1 Thu Sep 05 01:58:48 2013 +0200
1.2 +++ b/Admin/components/components.sha1 Thu Sep 05 12:33:51 2013 +0200
1.3 @@ -31,6 +31,7 @@
1.4 8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
1.5 06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
1.6 c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
1.7 +5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
1.8 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
1.9 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
1.10 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
2.1 --- a/Admin/components/main Thu Sep 05 01:58:48 2013 +0200
2.2 +++ b/Admin/components/main Thu Sep 05 12:33:51 2013 +0200
2.3 @@ -4,7 +4,7 @@
2.4 exec_process-1.0.3
2.5 Haskabelle-2013
2.6 jdk-7u21
2.7 -jedit_build-20130628
2.8 +jedit_build-20130905
2.9 jfreechart-1.0.14
2.10 kodkodi-1.5.2
2.11 polyml-5.5.0-3
3.1 --- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 05 01:58:48 2013 +0200
3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 05 12:33:51 2013 +0200
3.3 @@ -221,6 +221,7 @@
3.4 "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
3.5 "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
3.6 "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
3.7 + "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
3.8 )
3.9
3.10 declare -a JFREECHART_JARS=()
4.1 --- a/src/Tools/jEdit/patches/jedit/annotation Thu Sep 05 01:58:48 2013 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,45 +0,0 @@
4.4 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/input/AbstractInputHandler.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/input/AbstractInputHandler.java
4.5 ---- 5.0.0/jEdit/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-11-17 16:41:23.000000000 +0100
4.6 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-12-01 18:40:31.000000000 +0100
4.7 -@@ -29,8 +29,6 @@
4.8 - import java.awt.event.KeyEvent;
4.9 - import java.util.Hashtable;
4.10 - import java.util.StringTokenizer;
4.11 --import javax.annotation.Nonnull;
4.12 --import javax.annotation.Nullable;
4.13 -
4.14 - import org.gjt.sp.jedit.JEditAbstractEditAction;
4.15 - import org.gjt.sp.jedit.gui.ShortcutPrefixActiveEvent;
4.16 -@@ -198,8 +196,7 @@
4.17 - * @param keyBinding The key binding
4.18 - * @since jEdit 3.2pre5
4.19 - */
4.20 -- @Nullable
4.21 -- public Object getKeyBinding(@Nonnull String keyBinding)
4.22 -+ public Object getKeyBinding(String keyBinding)
4.23 - {
4.24 - Hashtable current = bindings;
4.25 - StringTokenizer st = new StringTokenizer(keyBinding);
4.26 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
4.27 ---- 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 2012-11-17 16:42:29.000000000 +0100
4.28 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2012-12-01 18:40:40.000000000 +0100
4.29 -@@ -35,8 +35,6 @@
4.30 - import org.gjt.sp.jedit.View.ViewConfig;
4.31 - import org.gjt.sp.jedit.bsh.UtilEvalError;
4.32 -
4.33 --import javax.annotation.Nonnull;
4.34 --import javax.annotation.Nullable;
4.35 - import javax.swing.*;
4.36 - import java.awt.event.*;
4.37 - import java.io.*;
4.38 -@@ -3853,8 +3851,7 @@
4.39 -
4.40 - } //}}}
4.41 -
4.42 -- @Nonnull
4.43 -- private static String getPLAFClassName(@Nullable String lf)
4.44 -+ private static String getPLAFClassName(String lf)
4.45 - {
4.46 - if (lf != null && lf.length() != 0)
4.47 - {
4.48 -
5.1 --- a/src/Tools/jEdit/patches/jedit/brackets Thu Sep 05 01:58:48 2013 +0200
5.2 +++ b/src/Tools/jEdit/patches/jedit/brackets Thu Sep 05 12:33:51 2013 +0200
5.3 @@ -1,5 +1,6 @@
5.4 ---- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2012-11-17 16:42:29.000000000 +0100
5.5 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-08-24 15:58:43.075546141 +0200
5.6 +diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
5.7 +--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
5.8 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +0200
5.9 @@ -97,6 +97,22 @@
5.10 case '}': if (direction != null) direction[0] = false; return '{';
5.11 case '<': if (direction != null) direction[0] = true; return '>';
6.1 --- a/src/Tools/jEdit/patches/jedit/completion Thu Sep 05 01:58:48 2013 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,15 +0,0 @@
6.4 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java
6.5 ---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 2012-11-17 16:41:58.000000000 +0100
6.6 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java 2013-01-04 14:25:57.095172180 +0100
6.7 -@@ -113,9 +113,9 @@
6.8 - list.setCellRenderer(new CellRenderer());
6.9 - list.addKeyListener(keyHandler);
6.10 - list.addMouseListener(new MouseHandler());
6.11 -+ list.setFocusTraversalKeysEnabled(false);
6.12 -
6.13 - JPanel content = new JPanel(new BorderLayout());
6.14 -- content.setFocusTraversalKeysEnabled(false);
6.15 - // stupid scrollbar policy is an attempt to work around
6.16 - // bugs people have been seeing with IBM's JDK -- 7 Sep 2000
6.17 - JScrollPane scroller = new JScrollPane(list,
6.18 -
7.1 --- a/src/Tools/jEdit/patches/jedit/extended_styles Thu Sep 05 01:58:48 2013 +0200
7.2 +++ b/src/Tools/jEdit/patches/jedit/extended_styles Thu Sep 05 12:33:51 2013 +0200
7.3 @@ -1,6 +1,6 @@
7.4 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
7.5 ---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2012-11-17 16:41:58.000000000 +0100
7.6 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2012-12-01 17:34:47.000000000 +0100
7.7 +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
7.8 +--- 5.1.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2013-07-28 19:03:38.000000000 +0200
7.9 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2013-09-05 10:51:29.192192327 +0200
7.10 @@ -79,7 +79,7 @@
7.11 start = next;
7.12 token = token.next;
7.13 @@ -10,9 +10,9 @@
7.14 {
7.15 JOptionPane.showMessageDialog(textArea.getView(),
7.16 jEdit.getProperty("syntax-style-no-token.message"),
7.17 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
7.18 ---- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2012-11-17 16:42:25.000000000 +0100
7.19 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2012-12-01 18:28:35.000000000 +0100
7.20 +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
7.21 +--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2013-07-28 19:03:51.000000000 +0200
7.22 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2013-09-05 10:51:29.192192327 +0200
7.23 @@ -256,9 +256,9 @@
7.24 //{{{ Package private members
7.25
7.26 @@ -34,9 +34,9 @@
7.27 private GlyphVector[] glyphs;
7.28 //}}}
7.29
7.30 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
7.31 ---- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2012-11-17 16:42:25.000000000 +0100
7.32 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2012-12-01 17:37:04.000000000 +0100
7.33 +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
7.34 +--- 5.1.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2013-07-28 19:03:51.000000000 +0200
7.35 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2013-09-05 10:51:29.192192327 +0200
7.36 @@ -57,7 +57,7 @@
7.37 */
7.38 public static String tokenToString(byte token)
7.39 @@ -46,9 +46,9 @@
7.40 } //}}}
7.41
7.42 //{{{ Token types
7.43 -diff -ru 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
7.44 ---- 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2012-11-17 16:42:30.000000000 +0100
7.45 -+++ 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2012-12-01 17:40:33.000000000 +0100
7.46 +diff -ru 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
7.47 +--- 5.1.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2013-07-28 19:03:53.000000000 +0200
7.48 ++++ 5.1.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2013-09-05 10:51:29.192192327 +0200
7.49 @@ -194,7 +194,24 @@
7.50 {
7.51 return loadStyles(family,size,true);
7.52 @@ -88,10 +88,10 @@
7.53 +
7.54 private SyntaxUtilities(){}
7.55 }
7.56 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
7.57 ---- 5.0.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-11-17 16:41:43.000000000 +0100
7.58 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-12-01 17:28:12.000000000 +0100
7.59 -@@ -906,6 +906,11 @@
7.60 +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
7.61 +--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
7.62 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-05 10:51:29.196192309 +0200
7.63 +@@ -907,6 +907,11 @@
7.64 return chunkCache.getLineInfo(screenLine).physicalLine;
7.65 } //}}}
7.66
7.67 @@ -103,4 +103,3 @@
7.68 //{{{ getScreenLineOfOffset() method
7.69 /**
7.70 * Returns the screen (wrapped) line containing the specified offset.
7.71 -
8.1 --- a/src/Tools/jEdit/patches/jedit/macos Thu Sep 05 01:58:48 2013 +0200
8.2 +++ b/src/Tools/jEdit/patches/jedit/macos Thu Sep 05 12:33:51 2013 +0200
8.3 @@ -1,43 +1,13 @@
8.4 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
8.5 ---- 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 2012-11-17 16:42:29.000000000 +0100
8.6 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java 2012-12-01 17:32:47.000000000 +0100
8.7 -@@ -318,6 +318,10 @@
8.8 - {
8.9 - os = WINDOWS_NT;
8.10 - }
8.11 -+ else if(osName.contains("Mac OS X"))
8.12 -+ {
8.13 -+ os = MAC_OS_X;
8.14 -+ }
8.15 - else if(osName.contains("VMS"))
8.16 - {
8.17 - os = VMS;
8.18 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
8.19 ---- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 2012-11-17 16:42:29.000000000 +0100
8.20 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-01-04 20:00:25.698332853 +0100
8.21 +diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
8.22 +--- 5.1.0/jEdit/org/gjt/sp/jedit/Debug.java 2013-07-28 19:03:49.000000000 +0200
8.23 ++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-09-05 10:55:36.388181955 +0200
8.24 @@ -109,7 +109,7 @@
8.25 - * used to handle a modifier key press in conjunction with an alphabet
8.26 - * key. <b>On by default on MacOS.</b>
8.27 - */
8.28 -- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
8.29 -+ public static boolean ALTERNATIVE_DISPATCHER = false;
8.30 + * used to handle a modifier key press in conjunction with an alphabet
8.31 + * key. <b>On by default on MacOS.</b>
8.32 + */
8.33 +- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
8.34 ++ public static boolean ALTERNATIVE_DISPATCHER = false;
8.35
8.36 - /**
8.37 - * If true, A+ shortcuts are disabled. If you use this, you should also
8.38 -diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.0.0/jEdit-patched/org/gjt/sp/jed
8.39 -it/gui/KeyEventWorkaround.java
8.40 ---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2012-11-17 16:41:58.000000000 +0100
8.41 -+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-01-04 20:04:43.02632209
8.42 -2 +0100
8.43 -@@ -297,8 +297,8 @@
8.44 -
8.45 - if(!Debug.ALTERNATIVE_DISPATCHER)
8.46 - {
8.47 -- if(((modifiers & InputEvent.CTRL_MASK) != 0
8.48 -- ^ (modifiers & InputEvent.ALT_MASK) != 0)
8.49 -+ if((modifiers & InputEvent.CTRL_MASK) != 0 && (modifiers & InputEvent.ALT_MASK) == 0
8.50 -+ || (modifiers & InputEvent.CTRL_MASK) == 0 && (modifiers & InputEvent.ALT_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED
8.51 - || (modifiers & InputEvent.META_MASK) != 0)
8.52 - {
8.53 - return null;
8.54 + /**
8.55 + * If true, A+ shortcuts are disabled. If you use this, you should also
8.56