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

On Fri, 27 Jul 2012, Tjark Weber wrote:

Nitpick's output frequently contains subscripts: e.g., "a⇘1⇙"

With Isabelle/jEdit (2012, Linux), these are not displayed properly on
my system: the arrows are merely shown as black rectangles in the jEdit
Output pane.

Black rectangles mean you have an old version of the IsabelleText font hanging around on your system, such as ~/.fonts/ on Linux. Better delete that, or if you really think you need it indepedently of Isabelle/jEdit, copy afresh from Isabelle2012/lib/fonts/.

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

Generally, the block version of sub/superscript display is presently in this poor-man's form with arrows instead of style change. There are conceptual problems behind this -- even in Proof General 3.x/4.x its display was only approximative.

De-facto there are very few applications of that feature anyway, so this detail can stay at low priority for some time.


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