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


I’d be glad if anyone could answer at least some of the questions I
raised in my e-mail below. I’d like to write the documentation of my
Isabelle code properly, for which feedback on these matters would be
necessary. Thanks in advance.

All the best,

Am Dienstag, den 11.06.2019, 22:13 +0300 schrieb Wolfgang Jeltsch:
> Hello!
> 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.
> 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?
> 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>‹…›`.
> 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? 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?
> All the best,
> Wolfgang

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