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

Am Samstag, den 06.07.2019, 20:32 +1000 schrieb Peter Gammie:
> > Hmm, when I enter a non-ASCII character into an Isabelle/jEdit
> > buffer, I cannot be sure that it will make it into the file in
> > UTF-8-encoded form when saving. I think it works in practice for
> > symbols like “ and ”. However, if I enter the Greek letter γ, for
> > example, it will be saved to the file as `\<gamma>`. If it appears
> > in documentation text, outside of actual Isabelle code, this
> > `\<gamma>` will end up verbatim in the generated LaTeX source code,
> > causing an error.
> 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.

That would be correct only when these symbols are Isabelle identifiers.
For writing something like “π-calculus” or “η-expansion”, it would be
semantically incorrect (although it would produce the correct output).

> > So apparently it would work to place a symbol like “ or ” into the
> > documentation part of an Isabelle file and having it transferred to
> > the generated LaTeX file and finally processed correctly by LaTeX
> > using some sort of LaTeX UTF-8 support. However, this would work
> > only because symbols like “ and ” don’t have an Isabelle encoding in
> > the form `\<…>`. As soon as they’d get one, we would run into the
> > same problem as with the γ above.
> Indeed. You could define your own Isabelle symbols for these, but I’m
> not sure it’ll look great. How about the standard LaTeX `` ''?

I think that’s the way to go for now.

So my conclusion is:

  * Use antiquotations whenever you embed Isabelle code into the
    documentation text.

  * Use antiquotations for markup (for example, for lists and URLs).

  * Use LaTeX source code otherwise, particularly for non-ASCII symbols
    in text (for example, ~ for no-break spaces and '' for ”).

All the best,

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