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

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 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.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8297296166419983, "perplexity": 3670.9797707311636}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.3, "absolute_threshold": 10, "end_threshold": 5, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-31/segments/1627046154356.39/warc/CC-MAIN-20210802172339-20210802202339-00443.warc.gz"}