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

[Rafal Kolanski]

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:
> 
> * jEdit-5.3.0 has been released a few weeks ago, and we are using it since
>   Isabelle/d40f906bb13f.
> 
> * I am still waiting for various plugin updates, notably Navigator.
> 
> * There are still some fine points to be ironed out in main jEdit and some
>   plugins, i.e. bad GUI rendering on very high resolution displays.
> 
> This means there will be a few small changes to the jedit_build
> components, based on what the official jEdit project provides in the
> coming weeks.

This will not include any of my changes as no one has looked at my
patches to jEdit since however many months ago I submitted them.

> Concerning the font substitution approach: Did you rethink my proposal
> to use the python interface of fontforge to assemble Isabelle font
> derivatives systematically?

So, concerning this situation, you are right and the correct way to go
about font substitution is not to do it, or do it offline. Java's font
substitution system is too poor to do what we want without massive
effort. I am looking at the python+fontforge route, but making slow
progress so far due to work commitments interrupting.

However, that does not change the fact that your way of splitting chunks
into little pieces every time you encounter an Isabelle symbol is
inefficient. The patch I sent out in "Font substitution and handling in
Isabelle/jEdit" on the 3rd of September contains a change, along with a
small change to jEdit to expose some extra information.

As I already stated multiple times in the past, that change needs to
address font substitution because font substitution is a feature in
jEdit. If someone enables it, then your rendering of chunks must still
match up with jEdit's rendering of chunks, because you are overlaying
one on the other. You currently split the chunks needlessly and use lots
of IDs regardless of font substitution being enabled or not.

With my change, font substitution still works, sure, but the important
thing is it renders the entire jEdit chunk with a single call when font
substitution is disabled. This simplifies memory layout and rendering
code in the most common case which is the only case you want to support
(i.e. everyone using IsabelleText font only).

I really cannot say anything more unless you look at the patch I sent
and see how the code changes. I don't know why that is not possible.

> This would allow applications to use just one font.  Thus the special
> tricks of the jEdit text area won't be required.  The result would also
> work with plain Java Swing components, or in a completely different GUI
> context (e.g. a web browser).

Yes, and if you rip out font substitution from jEdit entirely, then my
patch to rendering simplifies even more.

> Note that the Isabelle-generated HTML pages already include the Isabelle
> fonts since Isabelle/b3c665940d62 (and a few later changes).  Other
> fonts could be used as well, by modifications in the CSS.
> 
> Thus we have a chance to get a uniform approach to Isabelle symbol
> fonts, generated offline by some administrative python script.

Sure, and generating these fonts offline will allow crazy people like me
to have their own font which still includes all the glyphs necessary,
satisfying both you and I.

I will spend some evenings this week looking at scripting fontforge to
generate IsabelleText. Could you please take a little while to look at
my changes? I'm completely open to the idea of you not liking them and
requesting further changes or rejecting them, but endless discussion
without even looking really seems a waste of time. If no one looks at
anything I do, then I can just keep a local fork going and keep quiet
about the changes.

Either way, I am not bringing this change up any more after this email,
and consider it "rejected without consideration", along with the jEdit
patches I submitted. For the record, all changes are still running along
without any problems months later, and have been stress tested by
working on the largest parts of the L4 verification project.

Sincerely,

Rafal Kolanski