[jedit:patches] #628 Font substitution sizes are not correctly loaded from settings
Rafal Kolanski via jEdit-devel <[email protected]>
| Newsgroups | gmane.editors.jedit.devel |
|---|---|
| Message-ID | </p/jedit/patches/628/9971d37f6fc718b6da6d7834f040692d9433a9c1.patches@jedit.p.sourceforge.net> |
Yes, you would know better when it is appropriate to mix the versions of the text area / jEdit... I clumsily imported whatever had the property loader. If you're OK duplicating it, then all good. You also noticed a redundant null check, which is nice. Thank you.
---
** [patches:#628] Font substitution sizes are not correctly loaded from settings**
**Status:** pending
**Group:**
**Created:** Sat Jun 26, 2021 12:27 AM UTC by Rafal Kolanski
**Last Updated:** Sun Sep 12, 2021 01:08 PM UTC
**Owner:** nobody
**Attachments:**
- [0001-fix-for-font-substitution-sizes-not-being-read-from-.patch](https://sourceforge.net/p/jedit/patches/628/attachment/0001-fix-for-font-substitution-sizes-not-being-read-from-.patch) (1.2 kB; text/x-patch)
A while back, I contributed a patch that let jEdit understand font sizes in addition to font families for selecting fallback fonts. This functionality got in, but subsequently something went wrong and the size properties are saved, but no longer loaded. Only the family is loaded.
For example, selecting Cambria Math 16 as a fallback font results in the following entries in `properties`:
view.fontSubstList.0=Cambria Math
view.fontSubstList.0size=17
view.fontSubstList.0style=0
Only the first of these is loaded, since the code does not use `jEdit.getFontProperty`, and hence the size/style is ignored (it uses the generic `props.getProperty`).
Attached is a patch with a proposal to address the issue by using `jEdit.getFontProperty`. It does mean that Chunk now imports jEdit, but if that's undesireable, perhaps there's a better import or a better place to put getFontProperty.
---
Sent from sourceforge.net because [email protected] 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.
--
-----------------------------------------------
jEdit Developers' List
[email protected]
https://lists.sourceforge.net/lists/listinfo/jedit-devel