src/Tools/jEdit/patches/extended_styles
author wenzelm
Wed, 22 Jun 2011 16:32:36 +0200
changeset 43506 bf7400573617
parent 43482 ebb90ff55b79
permissions -rw-r--r--
updated to jedit-4.4.1 and jedit_build-20110622;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43506
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     1
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
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     2
--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-21 01:28:56.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     3
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2011-06-22 16:07:32.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     4
@@ -78,7 +78,7 @@
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     5
 			start = next;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     6
 			token = token.next;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     7
 		}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     8
-		if (token.id == Token.END || token.id == Token.NULL)
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
     9
+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    10
 		{
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    11
 			JOptionPane.showMessageDialog(textArea.getView(),
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    12
 				jEdit.getProperty("syntax-style-no-token.message"),
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    13
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
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    14
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-21 01:29:10.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    15
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2011-06-22 16:02:07.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    16
@@ -380,7 +380,7 @@
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    17
 	// this is either style.getBackgroundColor() or
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    18
 	// styles[defaultID].getBackgroundColor()
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    19
 	private Color background;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    20
-	private String str;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    21
+	public String str;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    22
 	//private GlyphVector gv;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    23
 	private List<GlyphVector> glyphs;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    24
 	private boolean visible;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    25
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
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    26
--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java	2011-06-21 01:29:10.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    27
+++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2011-06-22 16:08:47.000000000 +0200
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43460
diff changeset
    28
@@ -57,7 +57,7 @@
43506
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    29
 	 */
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    30
 	public static String tokenToString(byte token)
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    31
 	{
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    32
-		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    33
+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    34
 	} //}}}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    35
 
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    36
 	//{{{ Token types
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    37
diff -ru 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    38
--- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2011-06-21 01:29:11.000000000 +0200
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    39
+++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2011-06-22 16:05:28.000000000 +0200
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43460
diff changeset
    40
@@ -194,6 +194,23 @@
43506
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    41
 	}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    42
 	
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    43
 	/**
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    44
+	 * Extended styles derived from the user-specified style array.
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    45
+	 */
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    46
+
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    47
+	public static class StyleExtender
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    48
+	{
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    49
+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    50
+		{
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    51
+			return styles;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    52
+		}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    53
+	}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    54
+	volatile private static StyleExtender _styleExtender = new StyleExtender();
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    55
+	public static void setStyleExtender(StyleExtender ext)
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    56
+	{
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    57
+		_styleExtender = ext;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    58
+	}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    59
+
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    60
+	/**
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    61
 	 * Loads the syntax styles from the properties, giving them the specified
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    62
 	 * base font family and size.
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    63
 	 * @param family The font family
43482
ebb90ff55b79 added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
wenzelm
parents: 43460
diff changeset
    64
@@ -222,8 +239,9 @@
43506
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    65
 				Log.log(Log.ERROR,StandardUtilities.class,e);
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    66
 			}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    67
 		}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    68
+		styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    69
 
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    70
-		return styles;
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    71
+		return _styleExtender.extendStyles(styles);
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    72
 	} //}}}
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    73
 	
bf7400573617 updated to jedit-4.4.1 and jedit_build-20110622;
wenzelm
parents: 43482
diff changeset
    74
 	private SyntaxUtilities(){}