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

[Makarius]

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.

   * 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).

   * 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.


> We do get a etc/symbols file, but it's a bit of an oddity. Unlike other 
> parts of Isabelle source code which use parser combinators, this is 
> thrown together with regular expressions.

That is really old, one of the very first modules of Isabelle/Scala.  It 
could have been updated to use Isabelle-style syntax, e.g. like session 
ROOT files.  One reason why I did not do it: Isabelle symbol encoding is 
conceptually like a regular Java string encoding.  Putting this at the 
very bottom of the JVM is possible, but extra library dependencies from 
Scala make it more difficult than necessary.

So maybe one day I will actually re-implement that in Java 8, which is the 
most recent functional programming language on the market.


> 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.


> 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.


 	Makarius