src/Tools/jEdit/patches/extended_styles_brackets

 +		case '⦉': if (direction != null) direction[0] = true;  return '⦊';
 +		case '⦊': if (direction != null) direction[0] = false; return '⦉';
  		default:  return '\0';
  		}
  	} //}}}
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2024-08-03 19:53:21.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2024-10-29 11:50:54.066016546 +0100
-@@ -357,8 +357,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(){}
- }