diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +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 jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2021-05-10 18:19:56.275495525 +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.
@@ -1622,8 +1627,8 @@
}
// Scan backwards, trying to find a bracket
- String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
- String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
+ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
+ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊";
int count = 1;
char openBracket = '\0';
char closeBracket = '\0';
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200
@@ -115,6 +115,8 @@
case '⦄': if (direction != null) direction[0] = false; return '⦃';
case '⟪': if (direction != null) direction[0] = true; return '⟫';
case '⟫': if (direction != null) direction[0] = false; return '⟪';
+ case '⦉': if (direction != null) direction[0] = true; return '⦊';
+ case '⦊': if (direction != null) direction[0] = false; return '⦉';
default: return '\0';
}
} //}}}
diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +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(){}
}