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


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.

> On 12 Jun 2019, at 05:13, Wolfgang Jeltsch <wolfgang-it at> wrote:
> 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.

> 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. 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.

Here’s an example: @{cite [cite_macro=citet] "Winskel:1993”}. Note that `citet` is a LaTeX macro — in this case a natbib one.

It seems that loading the corresponding BibTeX file into Isabelle/jEdit enables hyperlinks.

> 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.

> 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. Historically there were things like `text_raw` that suppressed the default Isabelle armour. See e.g. the possibly-obsolete

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.



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