On Sat, 3 Oct 2015, Rafal Kolanski wrote:
My priority at the moment is to see a release of jEdit, before we enter
the critical release phase for Isabelle2016 -- presumably at the start
of the Winter season here in the north.
Once it is there, I will update the jedit_build component
On 16/11/15 07:14, Makarius wrote:
> I have lost track of the status of this thread, with its various
> side-threads on isabelle-users, isabelle-dev, and private mail.
All the patches I have sent out are still in effect w.r.t font rendering.
> In the meantime the situation is as follows:
>
> *
On Tue, 15 Sep 2015, Rafal Kolanski wrote:
The patched jedit code base will be updated again for the coming
release of 5.3.0, which should appear *really*soon*now*. It will be
the first jEdit release with proper 4K display support!
Well, I hope they have time take a peek at some of the
On 03/10/15 00:35, Makarius wrote:
> On Tue, 15 Sep 2015, Rafal Kolanski wrote:
>
>>> The patched jedit code base will be updated again for the coming
>>> release of 5.3.0, which should appear *really*soon*now*. It will be
>>> the first jEdit release with proper 4K display support!
>>
>> Well, I
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
When I wanted to customize my symbol font when switching to JEdit, I
realized that:
1. 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
