Email Gateway (Aug 19 2022 at 07:59): Email Gateway (Aug 19 2022 at 07:59):From: Tjark Weber <webertj@in.tum.de>
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.
Best regards,
Tjark
Email Gateway (Aug 19 2022 at 07:59):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Tjark,
I can't solve the black rectangles, but the arrows are sure starting to get on my nerves. ;) See change be4bf5f6b2ef.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 07:59):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 19 2022 at 07:59):From: Tjark Weber <webertj@in.tum.de>
On Fri, 2012-07-27 at 15:52 +0200, Makarius wrote:
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/.
Thanks, that fixed the arrows.
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.
Best regards,
Tjark
Email Gateway (Aug 19 2022 at 07:59):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 08:00):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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).
Email Gateway (Aug 19 2022 at 08:00):From: Makarius <makarius@sketis.net>
Let's see it as a project to find out "conformance to Unicode", which is
generally not a hard-and-fast concept.
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.
The first column should give you glyphs according to Appendix B of
http://isabelle.in.tum.de/dist/Isabelle2012/doc/isar-ref.pdf -- or you
just compare to the IsabelleText version with jEdit, which might require
some tricks to get another copy running with the different font.
Makarius
Email Gateway (Aug 19 2022 at 08:00):From: Makarius <makarius@sketis.net>
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.
Makarius
symbols
Last updated: Apr 26 2024 at 08:19 UTC