Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Custom fonts in browser_info html?


view this post on Zulip Email Gateway (Jan 03 2021 at 12:03):

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

view this post on Zulip Email Gateway (Jan 08 2021 at 04:10):

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

view this post on Zulip Email Gateway (Jan 08 2021 at 15:29):

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: Dec 08 2021 at 08:24 UTC