#628 Font substitution sizes are not correctly loaded from settings
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.
Hi, there is a little problem here, the Chunk class cannot use jEdit class methods because it is part of the StandaloneTextArea package, it use only IPropertyManager. I think a simple solution would be to create a static method doing the job done in getFontProperty to decode the String ?
In fact what do you think of that version (I just added the getFontProperty code to the interface) I know there is some redundancy but I am not sure how I could remove it in a nice way.
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.