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

Le Fri, 27 Jul 2012 15:52:53 +0200, Makarius <makarius at> a écrit:

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

For people who get one, is it OK to use Cambria Math instead of the Isabelle font? Looks OK to me, but I prefer to be sure this cannot lead to error due to characters misinterpretation (if both are conform Unicode fonts, this should be really the same).

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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