[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts

[Rafal Kolanski]

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 system). It
>> even lets you specify font sizes so their metrics match!
> 
>> The Isabelle plugin doesn't use it.
> 
> This font-replacement mechanism is a relatively recent addition to jEdit
> from a few years ago. The Isabelle/jEdit treatment of symbols, fonts,
> text rendering preceeds that by 1 or 2 years.  When the jEdit guys added
> that feature, I noted it down on my TODO list immediately to revisit my
> own approach.  So far it did not happen for various reasons:
>
>   * Font replacement only affects text area derivatives.  For basic GUI
>     components it does not have any effect.  We have some ugly tricks like
>     using HTML and IsabelleText font in some places, e.g. Sidekick entry
>     titles.  Relying too much on font replacement would render that even
>     worse relatively to the text area.

I hope you have time to take a look at my suggestion (jEdit patch
submitted upstream plus changes to Isabelle/jEdit rendering posted to
the list on the 3rd of September). It addresses the issue of matching
jEdit's substitution during rendering text area derivatives, and reduces
chunk-splitting significantly.

For basic components I do not presently have a solution. GTK2/3 just
does a system-wide search to find missing glyphs, and Qt plugs into
that, but the JDK doesn't. Maybe someday.

>   * The jEdit "Chunk" concept (text tokens to be rendered eventually) is a
>     bit odd.  Looking myself too closely at it has a real danger of
>     spending a lot of time there to rework it.  I still want to do it
>     someday, but it does not have top priority at the moment, in contrast
>     to things like proper GUI scaling (for "4K"  displays on Windows and
>     Linux).

I have not used jEdit long enough to decide how well the concept is
executed, but the "chunk" setup seems not unusual for modern editors. If
you were to do it again, which approach would you prefer?

>   * Java 6 on Mac OS X had its own super-smart font-replacement, and my
>     main work machine at that time was that platform.  A bit too many
>     problems with such not-fully-working add-ons descreased the priority
>     further.  Now we have standard Java 8 even on Mac OS X, and it
>     probably does not get in the way anymore, but I did not check it.

On Linux (Ubuntu), I have not seen any form of font-replacement happen
on the JDK for at least Java7/8. I do not recall it happening ever, so
it may be a special OS X tweak.

> [...]
>> The lookup system then depends on compressing a maximum of two fonts
>> plus other meta information (subscript, superscript, bold) for every
>> JEdit chunk type (19 types) into a single Java byte... which is
>> signed, so 127 tags is maximum. Is this done for speed?
> 
> Presumed "speed" is a lame reason for anything.  I guess that Slava
> Pestov simply did not know better when he made that many years ago. 
> There are a few more oddities at the bottom of text area and buffer
> management, e.g. odd "split arrays" taken from Emacs.  Without thise
> mutable data non-sense -- with bytes, chars, arrays at the bottom --
> jEdit could be much faster and more scalable.

This is a misunderstanding, the question was referring to why you did it
that way, and after doing the work to implement the font substitution
functionality, I understand now (and tried to document it as best I
could in my long post on fonts/rendering).

jEdit is strange to me in various ways. The type questions I get is "hey
Raf, can you make parenthesis highlighting work in the output buffer?",
or "why can't we pop over to the output/query window and select stuff
with keyboard?". The answer is "not without modifying jEdit to add a
virtual EditPane that allows sending keystrokes to a text area that
isn't in an EditPane, otherwise jEdit will send it to the last active
EditPane even though it's not focused" etc.

>> It's a bit of a shock to new users that after they specify their fonts
>> the way they like, when JEdit loads everything looks great for a few
>> seconds, and then most symbols turns to rectangles when the Isabelle
>> plugin loads.
> 
> I doubt that new users will specify fonts "the way they like".  jEdit is
> so flexible, that it can be configured in ways that Isabelle/jEdit no
> longer works properly. We ship sane defaults, with a clear bias to
> support one standard way that works well.  Even just that is already
> difficult to maintain.

I know you are hesitant, but please take a look at the text area font
substitution code I sent out if/when you have time. It does not affect
existing features as shipped, except for a bit of improved memory
efficiency due to less chunk splitting. It also frees up some IDs you
can use for two levels of sub/superscript, which is a feature Gerwin has
been asking me for (and bsub/bsup).

The "unsurprising" part refers to the text area font substitution
working when engaged, as compared to it ignoring you. Sure, there are
one or two consequences, but they are the "you pressed the big red
button didn't you" kind and not the "go away, we know better" kind.

Thank you for adding the space escape mechanism to etc/symbols and for
the constructive discussion! I wish I could just show you my changes
working and explain how they work in person, but we are slightly too far
for a coffee break meeting.

Sincerely,

Rafal Kolanski