Re: [isabelle] Non-ASCII characters and unsupported text structures

On 06/07/2019 12:32, Peter Gammie wrote:
> Err, right. So I think you’re supposed to say @{text “\<gamma>”} or even better, use @{const “…”} or @{term “…”} etc. for symbols that Isabelle knows about. There’s a list in the Isabelle repo/distribution `etc/symbols`.

The standard way to typeset formal text (without checking) inside
informal document source is just a cartouche, e.g. ‹α›. That is a short
form for \<^cartouche> with a single cartouche argument, it abbreviates
@{cartouche ...}, which in turn is an alias for the older @{text ...}.

As a general principle, each embedded language in Isabelle that uses
antiquotations as "one shot free" for such an implicit cartouche
operator. For example, the generated source in
$ISABELLE_HOME/src/Tools/Haskell uses that to refer to an ML expression
(of type string) that is meant to be inlined into the generated Haskell
source. e.g. ‹Markup.nameN›.

> Yes, you’d probably struggle to write Greek words in a `text` block.

Yes, this is because Unicode is a bit fragile: there are official math
greek slots, but using them is too ambitious. It is outside the 16-bit
range of UTF-16 (requiring surrogates that often cause problems). It
also means you would hardly ever see the correct glyphs outside the
Isabelle font context (e.g. in a mail client or on Stackoverflow).

It is a concession to quasi-portability to trade greek text for greek as
mathematical symbols.


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