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



Wolfgang,

> On 5 Jul 2019, at 03:07, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> wrote:
> 
> 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. There’s a list in the Isabelle repo/distribution `etc/symbols`.

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

> 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 it’s clear what needs doing from the `symbols` file and the LaTeX errors you’ll get.

> Hmm, so far I had assumed that all antiquotations are documented in the
> Isabelle/Isar Reference Manual, but apparently there are some that
> aren’t.

I’d get used to spelunking the source code. You can try in Isabelle/jEdit (try CMD/Ctrl-click on promising things) and follow it up with grep…

cheers,
peter

-- 
http://peteg.org/





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