--- a/src/Tools/jEdit/patches/extended_styles Wed Jun 10 15:55:41 2020 +0200
+++ b/src/Tools/jEdit/patches/extended_styles Wed Jun 10 19:59:12 2020 +0200
@@ -1,7 +1,7 @@
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2018-04-09 01:57:24.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2019-02-24 12:32:09.336643045 +0100
-@@ -322,9 +322,9 @@
+diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2020-06-09 17:01:03.000000000 +0200
++++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2020-06-10 15:38:59.771992636 +0200
+@@ -332,9 +332,9 @@
//{{{ Package private members
//{{{ Instance variables
@@ -13,19 +13,20 @@
//}}}
//{{{ Chunk constructor
-@@ -572,7 +572,7 @@
- // this is either style.getBackgroundColor() or
+@@ -585,7 +585,7 @@
// styles[defaultID].getBackgroundColor()
private Color background;
+- private char[] chars;
- private String str;
++ public char[] chars;
+ public String str;
- private GlyphVector[] glyphs;
+ private GlyphData glyphData;
//}}}
-diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-02-24 12:20:10.550459878 +0100
-@@ -917,6 +917,11 @@
+diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2020-05-20 11:10:10.000000000 +0200
++++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2020-06-10 15:38:03.605353644 +0200
+@@ -914,6 +914,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -37,15 +38,20 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2018-04-09 01:58:37.000000000 +0200
-+++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2019-02-24 12:20:10.550459878 +0100
-@@ -200,7 +200,24 @@
- {
- return loadStyles(family,size,true);
- }
--
-+
+diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2020-05-20 11:10:13.000000000 +0200
++++ 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2020-06-10 16:10:50.165837982 +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.
+ */
@@ -63,21 +69,5 @@
+ _styleExtender = ext;
+ }
+
- /**
- * Loads the syntax styles from the properties, giving them the specified
- * base font family and size.
-@@ -230,9 +247,11 @@
- Log.log(Log.ERROR,StandardUtilities.class,e);
- }
- }
--
-- 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);
- } //}}}
--
-+
private SyntaxUtilities(){}
}