|
From: Makarius <mak...@us...> - 2025-05-20 09:46:06
|
--- **[patches:#645] Standardize notable color properties wrt. getColorHexString** **Status:** open **Group:** **Created:** Tue May 20, 2025 09:46 AM UTC by Makarius **Last Updated:** Tue May 20, 2025 09:46 AM UTC **Owner:** nobody **Attachments:** - [a.patch](https://sourceforge.net/p/jedit/patches/645/attachment/a.patch) (4.3 kB; text/x-patch) This is an attempt to reduce redundant entries in user properties (file "properties" in the settings directory). The problem is that color defaults use RGB without ALPHA, but SyntaxUtilities.getColorHexString() will add a prefix "#ff" for that. Thus most color properties end up in the user properties file, even without an actual change of the value. The patch adjusts the default jEdit colors to coincide with the ARGB format of SyntaxUtilities.getColorHexString(). Note that this does not cover plugin properties: that would require more profound changes, for example to have getColorHexString() omit a redundant "#ff" prefix. --- Sent from sourceforge.net because jed...@li... is subscribed to https://sourceforge.net/p/jedit/patches/ To unsubscribe from further messages, a project admin can change settings at https://sourceforge.net/p/jedit/admin/patches/options. Or, if this is a mailing list, you can unsubscribe from the mailing list. |