src/Tools/jEdit/patches/jedit/extended_styles
changeset 50306 b655d2d0406d
parent 50305 8290dc6c8d7f
child 53415 9ebab8b7d73c
--- a/src/Tools/jEdit/patches/jedit/extended_styles	Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/patches/jedit/extended_styles	Sat Dec 01 19:51:43 2012 +0100
@@ -1,7 +1,7 @@
-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 @@
+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
+@@ -79,7 +79,7 @@
  			start = next;
  			token = token.next;
  		}
@@ -10,21 +10,33 @@
  		{
  			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 @@
+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
+@@ -256,9 +256,9 @@
+ 	//{{{ Package private members
+ 
+ 	//{{{ Instance variables
+-	SyntaxStyle style;
++	public SyntaxStyle style;
+ 	// set up after init()
+-	float width;
++	public float width;
+ 	//}}}
+ 
+ 	//{{{ Chunk constructor
+@@ -506,7 +506,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
+ 	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
 @@ -57,7 +57,7 @@
  	 */
  	public static String tokenToString(byte token)
@@ -34,9 +46,9 @@
  	} //}}}
  
  	//{{{ 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
+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
 @@ -194,7 +194,24 @@
  	{
  		return loadStyles(family,size,true);
@@ -76,3 +88,19 @@
 +
  	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 @@
+ 		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.
+