Not all fonts are the same pixel size for a given point size and
presumably the user wants the final metrics to match.
Given that now the user can specify preferred fallback font sizes, that
leaves system-fallback fonts, which don't come with size info. Since
java.awt.GraphicsEnvironment.getAllFonts returns a font size of 1, we
scale those fonts up to the main font point size.
So if you know what you're doing, you can set up fonts precisely the way
you like, and if you don't, you can just select the system font fallback
behavior and get the previous outcome.
While testing, I discovered an obscure situation which was not handled properly: when the font has a transformation assigned to it for some reason (e.g. a plugin deciding that a certain syntax style should be slanted/squashed/whatever), I was previously cancelling the transformation during the substitution font derivation as the original jEdit code did.
This updated version of the patch preserves any transforms applied to fonts when performing code point substitutions.
Last edit: Rafal Kolanski 2015-09-01
Plugin authors might want to conform to jEdit users' font substitution settings, but Chunk does not have enough information available. Additionally, as a plugin author trying to render some text in different colors over/instead of those in a Chunk, a bit of extra info is needed. We can do font substitution on our own, but when the user changes the settings, those in Chunk are updated immediately, making it the logical place to tweak.
In order to facilitate this functionality for plugin authors, I have refactored the font lookup (getSubstFont) and derivation (deriveSubstFont) code and made it public, as well as adding a method to check whether font substitution was used in a chunk at all.
I have done thorough testing with glyphs missing in the main font, the user substitution fonts, and the system fonts. I have also checked for sanity when using code points above 0xFFFF. Everything looks good as far as I can see.
This final version contains all the functionality I desired, both as a jEdit user and plugin coder. I am open to discussion, feedback and criticism!
Last edit: Rafal Kolanski 2015-09-04
I have used this patch for over a year without problems. I have rebased it onto the version I'm using (r24302) and used it successfully for months after that. If I get a thumbs down, well, so be it, but it's a bit sad when it's been this long without sight of thumbs...
I am unfamiliar with this code, and I was also not clear on how to test it, so I assigned it to Dale.
I am sorry it has taken me so long to look more closely at this.
In any case, I was wondering after I apply the patch (it applied cleanly), how do I test it?
I see no new option in the option pane.
Will this make things look better on high resolution screens automagically? that would be nice.
There is no new option in the option pane. It allows you to specify the sizes of the fallback fonts. For example, let's say your favourite font ever is Consolas, and you choose a 12pt size for it. Now, does Consolas have symbols for ⦃⦄, for example? Nope. So you select a fallback font that does have these. The font you select might not actually look the same size as Cambria at 12pt, so you might want to tweak it a little, making it smaller or bigger. With current jEdit, you cannot make that adjustment, but with my patch, you can.
See attachments for how the options look like, and for how some example text in the text buffer looks like. The symbols are rendered with multiple fonts, since none contains all of them, yet the result looks coherent. Please take a look and let me know if I can explain more.
Sadly, it will not help directly with high resolution screens, only with a feeling of font sizes being mismatched.
Since there is some interest again, I'll upload a rebased version of the patch in a bit. Thanks for reviving it. I put up 3 a long time ago, and nothing has happened on any of them despite my using them all the entire time, which made me a bit sad.
Last edit: Rafal Kolanski 2017-10-30
Committed revision 24775.
Thanks for your contribution!
I just discovered that this patch breaks the independent textarea.
compile-textArea:
[mkdir] Created dir: /home/jenkins/workspace/jEdit_TextArea/textarea/build
[javac] Compiling 227 source files to /home/jenkins/workspace/jEdit_TextArea/textarea/build
[javac] /home/jenkins/workspace/jEdit_TextArea/textarea/src/org/gjt/sp/jedit/syntax/Chunk.java:37: error: cannot find symbol
[javac] import org.gjt.sp.jedit.jEdit;
[javac] ^
[javac] symbol: class jEdit
[javac] location: package org.gjt.sp.jedit
[javac] /home/jenkins/workspace/jEdit_TextArea/textarea/src/org/gjt/sp/jedit/syntax/Chunk.java:245: error: cannot find symbol
[javac] Font f = jEdit.getFontProperty("view.fontSubstList." + i);
[javac] ^
[javac] symbol: variable jEdit
[javac] location: class Chunk
[javac] 2 errors
Matthieu, can you please fix this or suggest how to fix it in a comment here?
My apologies for missing this. I think the way to get around the references to jEdit in Chunk is to pass the information in via constructor. The question that comes to mind is whether Chunk font info is static once created, or whether it is dynamically modified when the user changes font options. I am unfamiliar with how the standalone textarea is intended to be used.
Hey, I added a missing property to jedit.props file, it seems the standalone textarea is fixed, but I don't think my fix is related with that 2 years old problem
This doesn't seem to be working on the latest version.
The actualy size of text rendered in alternative fonts is fixed, regardless of what size I set the font or even changing the size of the main one.
Glad I'm not the only one using the feature. Please see here:
https://sourceforge.net/p/jedit/patches/628/
also, you might be able to weigh in on the font "latching" during substitution at https://sourceforge.net/p/jedit/bugs/4114/