src/Tools/jEdit/patches/extended_styles
author wenzelm
Sat, 16 Jul 2011 20:14:58 +0200
changeset 43849 00f4b305687d
parent 43506 bf7400573617
permissions -rw-r--r--
access to process output stream via auxiliary fifo;

diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-21 01:28:56.000000000 +0200
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-22 16:07:32.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 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-21 01:29:10.000000000 +0200
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-22 16:02:07.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 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2011-06-21 01:29:10.000000000 +0200
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-22 16:08:47.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 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
--- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2011-06-21 01:29:11.000000000 +0200
+++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-22 16:05:28.000000000 +0200
@@ -194,6 +194,23 @@
 	}
 	
 	/**
+	 * 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.
 	 * @param family The font family
@@ -222,8 +239,9 @@
 				Log.log(Log.ERROR,StandardUtilities.class,e);
 			}
 		}
+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
 
-		return styles;
+		return _styleExtender.extendStyles(styles);
 	} //}}}
 	
 	private SyntaxUtilities(){}