Re: [isabelle] Nitpick Output/jEdit Support for Subscripts



On Fri, 27 Jul 2012, Tjark Weber wrote:

Note that the JVM can load fonts dynamically without any "installation", but having installed one already prevents loading another one under program control.

It is not possible to load a font from a font file, and to use it independently of the fonts installed already? JVM font management seems broken in more ways than one.

I don't call anything broken on the JVM. It is just very peculiar. Things like the above are the norm, not the exception.

It should be getting slightly better when Oracle ships the next Java 7 update for all three platforms (Windows, Linux, Mac OS) this summer. Then there will be only one uniform way of being odd.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.