src/Tools/jEdit/patches/extended_styles

update to official jedit-5.6.0;

diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-08 20:13:23.565140195 +0200
@@ -332,9 +332,9 @@
 	//{{{ Package private members
 
 	//{{{ Instance variables
-	SyntaxStyle style;
+	public SyntaxStyle style;
 	// set up after init()
-	float width;
+	public float width;
 	//}}}
 
 	//{{{ Chunk constructor
@@ -584,8 +584,8 @@
 	// this is either style.getBackgroundColor() or
 	// styles[defaultID].getBackgroundColor()
 	private Color background;
-	private char[] chars;
-	private String str;
+	public char[] chars;
+	public String str;
 	private GlyphData glyphData;
 	//}}}
 
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-08 20:13:23.569140077 +0200
@@ -914,6 +914,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 -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
--- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2020-09-03 05:31:09.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2020-09-08 20:13:23.569140077 +0200
@@ -344,8 +344,28 @@
 			}
 		}
 
-		return styles;
+		styles[0] =
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
+				null, new Font(family, 0, size));
+		return _styleExtender.extendStyles(styles);
 	} //}}}
 
+	/**
+	 * 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;
+	}
+
 	private SyntaxUtilities(){}
 }