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

[Makarius]

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 accordingly. 
>> Then we have a brief window of opportunity to add some small patches on 
>> top of the standard jEdit code base as part of the Isabelle 
>> distribution.
>
> Well, if you're already warning me that the window will be very small if 
> and when it happens, then I would like to endeavor to make it count.
>
> If you find yourself with some spare cycles, perhaps you can do a Linus 
> and take a look at my patch to Isabelle's font rendering to see if you 
> like at all as a concept (there's a nice simplification to the rendering 
> code in there in addition to the font substitution). If so, I can do 
> extra work to make it more palatable to you / the Isabelle code base. If 
> you don't like it, fair enough, and I'll just maintain a branch locally 
> for my colleagues to use.

I have lost track of the status of this thread, with its various 
side-threads on isabelle-users, isabelle-dev, and private mail.


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.


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

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

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.


 	Makarius