updated to jedit_build-20130905 which is based on jedit-5.1.0;
authorwenzelm
Thu Sep 05 12:33:51 2013 +0200 (2013-09-05)
changeset 534159ebab8b7d73c
parent 53411 ab4edf89992f
child 53416 3a67ed19b755
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.*;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/patches/jedit/annotation
src/Tools/jEdit/patches/jedit/brackets
src/Tools/jEdit/patches/jedit/completion
src/Tools/jEdit/patches/jedit/extended_styles
src/Tools/jEdit/patches/jedit/macos
     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