[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
makarius at sketis.net
Sun Nov 15 21:14:04 CET 2015
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
> 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
* 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
Concerning the font substitution approach: Did you rethink my proposal to
use the python interface of fontforge to assemble Isabelle font
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.
More information about the isabelle-dev