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

Am Montag, den 01.07.2019, 10:48 +1000 schrieb Peter Gammie:
> Wolfgang,
> I don’t know what the state of the art is, or where documentation
> things are headed, but I’ll try to give you some pointers anyway.

Dear Peter,

thanks a lot for your explanations. Below are my responses to them.

> > What is the recommended way of embedding non-ASCII characters in
> > ordinary text (headlines and paragraph contents)? In actual Isabelle
> > code, I have access to the “infinite number of non-ASCII symbols”
> > but not in ordinary text as far as I can see.
> The Isabelle docs suggest that UTF-8 is OK in these contexts. See (I
> think) the Isabelle/jEdit manual.
> > I know that I can embed LaTeX source code that produces the desired
> > symbols, but that seems too low-level to me. Is there a way to enter
> > characters like no-break spaces and proper quotation marks (“ and ”)
> > directly?
> I don’t know anything about entering these characters. I’d suggest you
> use your favourite editor on the thy file directly. I get the
> impression that modern LaTeX can eat UTF8 OK.
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.

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.

> > Another thing are structures that aren’t currently supported by
> > Isabelle’s markup language. In particular I wonder how to properly
> > embed citations. Sure, I can use LaTeX source code again, but I’m
> > wondering whether it’s also possible to have an Isabelle construct,
> > perhaps user-defined, like `\<cite>‹…›`.
> There is a `cite` antiquotation. Try completing on `print_` in
> Isabelle/jEdit. One of those will give you a list of antiquotations. 

Amazing! I had looked for antiquotations in the Isabelle/Isar Reference
Manual but somehow overlooked the part that talks about `\<^cite>`.
Strangely enough, `\<^cite>` doesn’t appear in the auto-completion list
(in Isabelle2018 at least).

> To figure out their arguments you can trawl the docs, grep the
> Isabelle source code, or grep the AFP. Once you get to some steady-
> state the NEWS file is handy.

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

> > Regarding LaTeX source code, I discovered that it is possible to
> > embed it directly into the contents of `text`, `section`, and such.
> > Is this intentional or is it just that it happens to work with the
> > current Isabelle implementation?
> AFAIK this is what everyone has always done and will be doing for a
> while yet. Makarius appears to be steadily adding more semi-formal
> markup (? - I might be misusing that term) — \<^item> being one thing
> that sticks in my mind, and the absence so far of a \label{..}
> replacement.

I really like this trend of having more and more markup for
documentation text.

> > On the other hand, there is the `\<latex>‹…›` construct, which
> > doesn’t seem to be documented (I found it via the IDE’s
> > completion mechanism). Is this construct preferred over just
> > embedding LaTeX source code? Does it differ from plain embedding?
> I don’t know. Perhaps try to find uses of `\<latex>` in the AFP or
> HOL.

There seems to be absolutely no occurrence of `\<latex>` in the Isabelle
standard library.

> I wonder why you found this construct but not the `cite`
> antiquotation. Perhaps that would be useful feedback on feature
> discovery / the utility of the documentation.

I found `\<latex>` only by accident in the completion pop-up window when
looking for something else. As I mentioned above, `\<^cite>` doesn’t
appear in the completion list, and the list of antiquotations in the
Isabelle/Isar Reference Manual is incomplete.

> cheers,
> peter

All the best,

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