From: Makarius <makarius@sketis.net>
A rather old thread, but still current: in the past few weeks I have reworked
the HTML output a lot, a some details might still change for Isabelle2021
(February 2021).
I don't forsee ways to specify fonts right now, but maybe you want to explain
your application. Which font, which glyphs are you using in particular?
Makarius
From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>
I guess I am something of a crank in this respect, but I have edited a custom copy of IsabelleDejaVuSansMono mainly with copies of existing glyphs inserted in the "free space” areas of UNICODE. This lets me do things like have several <= characters for different order-like applications and avoid both ugly maths and ambiguous syntax.
Obviously it would be easier if several isasymbols could be bound to the same glyph code in the symbols file.
Also have some composite glyphs, more maths alpha-numerics and other custom jobs.
It would also be nice if some of these custom glyphs could be used in variable names.
Brendan
From: Makarius <makarius@sketis.net>
This sounds like major changes to the standard setup. Can you show me this
edited font privately, so that I get a better idea what you found missing?
Makarius
Last updated: Jan 04 2025 at 20:18 UTC