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

On Sat, 28 Jul 2012, Makarius wrote:

As a quick test, you can open Isabelle2012/etc/symbols and say "Reload with Encoding" in jEdit, and the choose "UTF-8-Isabelle" instead of UTF8, which is normally the default for that file.

Doing this myself on a remote Windows 2008 machine, I've found a few dropouts in Cambria Math, which are not very serious, though.

The included symbols file repairs them to some extent, via remapping to IsabelleText. If you put that in .isabelle/etc/symbols in your home directory and restart Isabelle/jEdit, the main text buffer will know these replacements, but not the Output window nor any popups -- they are bound to just one font.

How did I produce that table? After switching to the font in question and changing the encoding of etc/symbols to UTF-8-Isabelle, every line that looks bad is retained, any other line deleted. Then the file is saved in a different spot, to retain the original table, and the column with property "font: IsabelleText" is added.

#some re-assigments to repair Cambria Math drop-outs

#missing glyphs:
\<Midarrow>             code: 0x002550  font: IsabelleText
\<diamond>              code: 0x0025c7  font: IsabelleText
\<triangleleft>         code: 0x0025c3  font: IsabelleText
\<triangleright>        code: 0x0025b9  font: IsabelleText
\<clubsuit>             code: 0x002663  font: IsabelleText
\<diamondsuit>          code: 0x002662  font: IsabelleText
\<flat>                 code: 0x00266d  font: IsabelleText
\<natural>              code: 0x00266e  font: IsabelleText
\<sharp>                code: 0x00266f  font: IsabelleText
\<^bold>                code: 0x002759  font: IsabelleText  abbrev: -.

#swapped assignment of big vs. small version?!
\<oplus>                code: 0x002295  font: IsabelleText  abbrev: +o
\<Oplus>                code: 0x002a01  font: IsabelleText  abbrev: +O
\<otimes>               code: 0x002297  font: IsabelleText  abbrev: *o
\<Otimes>               code: 0x002a02  font: IsabelleText  abbrev: *O
\<odot>                 code: 0x002299  font: IsabelleText  abbrev: .o
\<Odot>                 code: 0x002a00  font: IsabelleText  abbrev: .O

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