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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
