# HG changeset patch
# User wenzelm
# Date 1378377231 -7200
# Node ID 9ebab8b7d73c7e5b35b27bea8664f2cad658ec05
# Parent ab4edf89992fb3bb6f61e3ee4d3f99afd05cd2ba
updated to jedit_build-20130905 which is based on jedit-5.1.0;
added jsr305-2.0.0.jar from http://code.google.com/p/findbugs (via ivy cache), which is required to resolve javax.annotation.*;
diff -r ab4edf89992f -r 9ebab8b7d73c Admin/components/components.sha1
--- a/Admin/components/components.sha1 Thu Sep 05 01:58:48 2013 +0200
+++ b/Admin/components/components.sha1 Thu Sep 05 12:33:51 2013 +0200
@@ -31,6 +31,7 @@
8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
+5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
diff -r ab4edf89992f -r 9ebab8b7d73c Admin/components/main
--- a/Admin/components/main Thu Sep 05 01:58:48 2013 +0200
+++ b/Admin/components/main Thu Sep 05 12:33:51 2013 +0200
@@ -4,7 +4,7 @@
exec_process-1.0.3
Haskabelle-2013
jdk-7u21
-jedit_build-20130628
+jedit_build-20130905
jfreechart-1.0.14
kodkodi-1.5.2
polyml-5.5.0-3
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 05 01:58:48 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Sep 05 12:33:51 2013 +0200
@@ -221,6 +221,7 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
"$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
+ "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
)
declare -a JFREECHART_JARS=()
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/patches/jedit/annotation
--- a/src/Tools/jEdit/patches/jedit/annotation Thu Sep 05 01:58:48 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-11-17 16:41:23.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-12-01 18:40:31.000000000 +0100
-@@ -29,8 +29,6 @@
- import java.awt.event.KeyEvent;
- import java.util.Hashtable;
- import java.util.StringTokenizer;
--import javax.annotation.Nonnull;
--import javax.annotation.Nullable;
-
- import org.gjt.sp.jedit.JEditAbstractEditAction;
- import org.gjt.sp.jedit.gui.ShortcutPrefixActiveEvent;
-@@ -198,8 +196,7 @@
- * @param keyBinding The key binding
- * @since jEdit 3.2pre5
- */
-- @Nullable
-- public Object getKeyBinding(@Nonnull String keyBinding)
-+ public Object getKeyBinding(String keyBinding)
- {
- Hashtable current = bindings;
- StringTokenizer st = new StringTokenizer(keyBinding);
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2012-12-01 18:40:40.000000000 +0100
-@@ -35,8 +35,6 @@
- import org.gjt.sp.jedit.View.ViewConfig;
- import org.gjt.sp.jedit.bsh.UtilEvalError;
-
--import javax.annotation.Nonnull;
--import javax.annotation.Nullable;
- import javax.swing.*;
- import java.awt.event.*;
- import java.io.*;
-@@ -3853,8 +3851,7 @@
-
- } //}}}
-
-- @Nonnull
-- private static String getPLAFClassName(@Nullable String lf)
-+ private static String getPLAFClassName(String lf)
- {
- if (lf != null && lf.length() != 0)
- {
-
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/patches/jedit/brackets
--- a/src/Tools/jEdit/patches/jedit/brackets Thu Sep 05 01:58:48 2013 +0200
+++ b/src/Tools/jEdit/patches/jedit/brackets Thu Sep 05 12:33:51 2013 +0200
@@ -1,5 +1,6 @@
---- 5.0.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-08-24 15:58:43.075546141 +0200
+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 '>';
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/patches/jedit/completion
--- a/src/Tools/jEdit/patches/jedit/completion Thu Sep 05 01:58:48 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/CompletionPopup.java 2012-11-17 16:41:58.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/CompletionPopup.java 2013-01-04 14:25:57.095172180 +0100
-@@ -113,9 +113,9 @@
- list.setCellRenderer(new CellRenderer());
- list.addKeyListener(keyHandler);
- list.addMouseListener(new MouseHandler());
-+ list.setFocusTraversalKeysEnabled(false);
-
- JPanel content = new JPanel(new BorderLayout());
-- content.setFocusTraversalKeysEnabled(false);
- // stupid scrollbar policy is an attempt to work around
- // bugs people have been seeing with IBM's JDK -- 7 Sep 2000
- JScrollPane scroller = new JScrollPane(list,
-
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/patches/jedit/extended_styles
--- a/src/Tools/jEdit/patches/jedit/extended_styles Thu Sep 05 01:58:48 2013 +0200
+++ b/src/Tools/jEdit/patches/jedit/extended_styles Thu Sep 05 12:33:51 2013 +0200
@@ -1,6 +1,6 @@
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2012-11-17 16:41:58.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2012-12-01 17:34:47.000000000 +0100
+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;
@@ -10,9 +10,9 @@
{
JOptionPane.showMessageDialog(textArea.getView(),
jEdit.getProperty("syntax-style-no-token.message"),
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2012-11-17 16:42:25.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2012-12-01 18:28:35.000000000 +0100
+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
@@ -34,9 +34,9 @@
private GlyphVector[] glyphs;
//}}}
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2012-11-17 16:42:25.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2012-12-01 17:37:04.000000000 +0100
+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)
@@ -46,9 +46,9 @@
} //}}}
//{{{ Token types
-diff -ru 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2012-11-17 16:42:30.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2012-12-01 17:40:33.000000000 +0100
+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);
@@ -88,10 +88,10 @@
+
private SyntaxUtilities(){}
}
-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
---- 5.0.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-11-17 16:41:43.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-12-01 17:28:12.000000000 +0100
-@@ -906,6 +906,11 @@
+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;
} //}}}
@@ -103,4 +103,3 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-
diff -r ab4edf89992f -r 9ebab8b7d73c src/Tools/jEdit/patches/jedit/macos
--- a/src/Tools/jEdit/patches/jedit/macos Thu Sep 05 01:58:48 2013 +0200
+++ b/src/Tools/jEdit/patches/jedit/macos Thu Sep 05 12:33:51 2013 +0200
@@ -1,43 +1,13 @@
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java 2012-12-01 17:32:47.000000000 +0100
-@@ -318,6 +318,10 @@
- {
- os = WINDOWS_NT;
- }
-+ else if(osName.contains("Mac OS X"))
-+ {
-+ os = MAC_OS_X;
-+ }
- else if(osName.contains("VMS"))
- {
- os = VMS;
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 2012-11-17 16:42:29.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2013-01-04 20:00:25.698332853 +0100
+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. On by default on MacOS.
- */
-- public static boolean ALTERNATIVE_DISPATCHER = OperatingSystem.isMacOS();
-+ public static boolean ALTERNATIVE_DISPATCHER = false;
+ * used to handle a modifier key press in conjunction with an alphabet
+ * key. On by default on MacOS.
+ */
+- 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
-diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 5.0.0/jEdit-patched/org/gjt/sp/jed
-it/gui/KeyEventWorkaround.java
---- 5.0.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2012-11-17 16:41:58.000000000 +0100
-+++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/KeyEventWorkaround.java 2013-01-04 20:04:43.02632209
-2 +0100
-@@ -297,8 +297,8 @@
-
- if(!Debug.ALTERNATIVE_DISPATCHER)
- {
-- if(((modifiers & InputEvent.CTRL_MASK) != 0
-- ^ (modifiers & InputEvent.ALT_MASK) != 0)
-+ if((modifiers & InputEvent.CTRL_MASK) != 0 && (modifiers & InputEvent.ALT_MASK) == 0
-+ || (modifiers & InputEvent.CTRL_MASK) == 0 && (modifiers & InputEvent.ALT_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED
- || (modifiers & InputEvent.META_MASK) != 0)
- {
- return null;
+ /**
+ * If true, A+ shortcuts are disabled. If you use this, you should also