# HG changeset patch
# User wenzelm
# Date 1354379030 -3600
# Node ID 8290dc6c8d7f4d0d98449b7a9de7125b65fb88ce
# Parent  21000e205d6cfc3eb3f0c7aaf351f302520f0674
more generic directory name to facilitate tracking changes of diffs;

diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit-4.5.2/caret
--- a/src/Tools/jEdit/patches/jedit-4.5.2/caret	Fri Nov 30 23:06:11 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2012-06-15 22:20:05.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2012-08-13 19:11:04.000000000 +0200
-@@ -4907,7 +4907,7 @@
- 	/**
- 	 * Returns true if the caret is visible, false otherwise.
- 	 */
--	final boolean isCaretVisible()
-+	public final boolean isCaretVisible()
- 	{
- 		return blink && hasFocus();
- 	} //}}}
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit-4.5.2/chunks
--- a/src/Tools/jEdit/patches/jedit-4.5.2/chunks	Fri Nov 30 23:06:11 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- jEdit/org/gjt/sp/jedit/textarea/TextArea.java       2012-08-13 19:11:04.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java       2012-09-03 19:37:48.000000000 +0200
-@@ -905,6 +905,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.
-
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit-4.5.2/extended_styles
--- a/src/Tools/jEdit/patches/jedit-4.5.2/extended_styles	Fri Nov 30 23:06:11 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
---- jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-06-15 22:20:11.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-08-13 19:13:59.000000000 +0200
-@@ -78,7 +78,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 jEdit/org/gjt/sp/jedit/syntax/Chunk.java jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-06-15 22:20:22.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-08-13 19:14:25.000000000 +0200
-@@ -380,7 +380,7 @@
- 	// this is either style.getBackgroundColor() or
- 	// styles[defaultID].getBackgroundColor()
- 	private Color background;
--	private String str;
-+	public String str;
- 	//private GlyphVector gv;
- 	private List<GlyphVector> glyphs;
- 	private boolean visible;
-diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
---- jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-06-15 22:20:22.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-08-13 19:14:44.000000000 +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 jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-06-15 22:20:25.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-08-13 19:19:20.000000000 +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 -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit-4.5.2/macos
--- a/src/Tools/jEdit/patches/jedit-4.5.2/macos	Fri Nov 30 23:06:11 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/OperatingSystem.java jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
---- jEdit/org/gjt/sp/jedit/OperatingSystem.java	2012-06-15 22:20:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java	2012-08-13 19:13:06.000000000 +0200
-@@ -317,6 +317,10 @@
- 			{
- 				os = OS2;
- 			}
-+			else if(osName.contains("Mac OS X"))
-+			{
-+				os = MAC_OS_X;
-+			}
- 			else if(osName.contains("VMS"))
- 			{
- 				os = VMS;
-diff -ru jEdit/org/gjt/sp/jedit/Debug.java jEdit-patched/org/gjt/sp/jedit/Debug.java
---- jEdit/org/gjt/sp/jedit/Debug.java	2012-06-15 22:20:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-08-13 19:44:43.000000000 +0200
-@@ -109,7 +109,8 @@
- 	 * 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 = OperatingSystem.isMacOS() &&
-+		System.getProperty("java.version").startsWith("1.6.");
- 
- 	/**
- 	 * If true, A+ shortcuts are disabled. If you use this, you should also
-
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit-4.5.2/memory
--- a/src/Tools/jEdit/patches/jedit-4.5.2/memory	Fri Nov 30 23:06:11 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java
---- jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java	2012-06-15 22:20:10.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java	2012-08-13 19:11:51.000000000 +0200
-@@ -222,7 +222,7 @@
- 		} //}}}
- 
- 		//{{{ Private members
--		private static final String memoryTestStr = "999/999Mb";
-+		private static final String memoryTestStr = "9999/9999Mb";
- 
- 		private final LineMetrics lm;
- 		private final Color progressForeground;
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit/caret
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/caret	Sat Dec 01 17:23:50 2012 +0100
@@ -0,0 +1,12 @@
+diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2012-06-15 22:20:05.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2012-08-13 19:11:04.000000000 +0200
+@@ -4907,7 +4907,7 @@
+ 	/**
+ 	 * Returns true if the caret is visible, false otherwise.
+ 	 */
+-	final boolean isCaretVisible()
++	public final boolean isCaretVisible()
+ 	{
+ 		return blink && hasFocus();
+ 	} //}}}
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit/chunks
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/chunks	Sat Dec 01 17:23:50 2012 +0100
@@ -0,0 +1,16 @@
+diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- jEdit/org/gjt/sp/jedit/textarea/TextArea.java       2012-08-13 19:11:04.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java       2012-09-03 19:37:48.000000000 +0200
+@@ -905,6 +905,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.
+
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit/extended_styles
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/extended_styles	Sat Dec 01 17:23:50 2012 +0100
@@ -0,0 +1,78 @@
+diff -ru jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
+--- jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2012-06-15 22:20:11.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2012-08-13 19:13:59.000000000 +0200
+@@ -78,7 +78,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 jEdit/org/gjt/sp/jedit/syntax/Chunk.java jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2012-06-15 22:20:22.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2012-08-13 19:14:25.000000000 +0200
+@@ -380,7 +380,7 @@
+ 	// this is either style.getBackgroundColor() or
+ 	// styles[defaultID].getBackgroundColor()
+ 	private Color background;
+-	private String str;
++	public String str;
+ 	//private GlyphVector gv;
+ 	private List<GlyphVector> glyphs;
+ 	private boolean visible;
+diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- jEdit/org/gjt/sp/jedit/syntax/Token.java	2012-06-15 22:20:22.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2012-08-13 19:14:44.000000000 +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 jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- jEdit/org/gjt/sp/util/SyntaxUtilities.java	2012-06-15 22:20:25.000000000 +0200
++++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2012-08-13 19:19:20.000000000 +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 -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit/macos
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/macos	Sat Dec 01 17:23:50 2012 +0100
@@ -0,0 +1,28 @@
+diff -ru jEdit/org/gjt/sp/jedit/OperatingSystem.java jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
+--- jEdit/org/gjt/sp/jedit/OperatingSystem.java	2012-06-15 22:20:24.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java	2012-08-13 19:13:06.000000000 +0200
+@@ -317,6 +317,10 @@
+ 			{
+ 				os = OS2;
+ 			}
++			else if(osName.contains("Mac OS X"))
++			{
++				os = MAC_OS_X;
++			}
+ 			else if(osName.contains("VMS"))
+ 			{
+ 				os = VMS;
+diff -ru jEdit/org/gjt/sp/jedit/Debug.java jEdit-patched/org/gjt/sp/jedit/Debug.java
+--- jEdit/org/gjt/sp/jedit/Debug.java	2012-06-15 22:20:24.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/Debug.java	2012-08-13 19:44:43.000000000 +0200
+@@ -109,7 +109,8 @@
+ 	 * 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 = OperatingSystem.isMacOS() &&
++		System.getProperty("java.version").startsWith("1.6.");
+ 
+ 	/**
+ 	 * If true, A+ shortcuts are disabled. If you use this, you should also
+
diff -r 21000e205d6c -r 8290dc6c8d7f src/Tools/jEdit/patches/jedit/memory
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/memory	Sat Dec 01 17:23:50 2012 +0100
@@ -0,0 +1,12 @@
+diff -ru jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java
+--- jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java	2012-06-15 22:20:10.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java	2012-08-13 19:11:51.000000000 +0200
+@@ -222,7 +222,7 @@
+ 		} //}}}
+ 
+ 		//{{{ Private members
+-		private static final String memoryTestStr = "999/999Mb";
++		private static final String memoryTestStr = "9999/9999Mb";
+ 
+ 		private final LineMetrics lm;
+ 		private final Color progressForeground;