On Tue, 25 Aug 2015, Rafal Kolanski wrote:
There is no separate symbol font setting, but JEdit does supply a nice
cascading font substitution system (if glyph not found in main font, try
next, then next, until optionally try every one in the system). It even
lets you specify font sizes so
On Tue, 25 Aug 2015, Rafal Kolanski wrote:
3. Trying to specify a font with a space in the name (e.g. Arial
Unicode MS, Cambria Math) doesn't work, because the config lines
in etc/symbols are split on \s+
See the following changeset:
changeset: 61174:74eddfef841e
tag: tip
user:
On 15/09/15 05:57, Makarius wrote:
> On Tue, 25 Aug 2015, Rafal Kolanski wrote:
>
>> - Removes hardcoded colors in favor of looking up relevant JEdit
>> properties. This is critical if you want a light-on-dark setup.
>> Also in patches/extended_styles style[0] is hardcoded to black
>> in
On 15/09/15 01:15, Makarius wrote:
> On Tue, 25 Aug 2015, Rafal Kolanski wrote:
>
>> There is no separate symbol font setting, but JEdit does supply a nice
>> cascading font substitution system (if glyph not found in main font,
>> try next, then next, until optionally try every one in the
