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

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Non-ASCII characters and unsupported text structures
• From: Peter Gammie <peteg42 at gmail.com>
• Date: Mon, 1 Jul 2019 10:48:11 +1000
• References: <00e199d103b5c14ceaf9ec569cf56c920b924f36.camel@jeltsch.info>

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.

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

> 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 https://isabelle.in.tum.de/community/Generate_TeX_Snippets

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.

cheers,
peter

--
http://peteg.org/



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