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

On 15/07/2019 18:32, Wolfgang Jeltsch wrote:
> Am Montag, den 15.07.2019, 15:34 +0200 schrieb Makarius:
>> A quick hypersearch (not grep) over $ISABELLE_HOME/src/Doc for
>> "utf|unicode" as insensitive regexp reveals the following explanation
>> in the Isabelle/jEdit manual:
>>> The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
>>> standard interpretation of finitely many symbols from the infinite
>>> collection. Uninterpreted symbols are displayed literally, e.g.\
>>> ``▩‹\<foobar>›''. Overlap of Unicode characters used in symbol
>>> interpretation with informal ones (which might appear e.g.\ in
>>> comments) needs to be avoided. Raw Unicode characters within prover 
>>> source files should be restricted to informal parts, e.g.\ to write 
>>> text in non-latin alphabets in comments.
> This snippet of an Isabelle comment reminds me of another question I
> wanted to ask: Is my assumption correct that a backslash followed by
> either a space or a newline with optionally some spaces afterwards is
> Isabelle’s representation of a no-break space and thus translated to a
> tilde when producing a LaTeX file?

The Isabelle document source language merely uses plain (La)TeX
conventions here: backslash-space and tilde occur like that in the
generated .tex output, their meaning is defined by Knuth and Lamport.
(You can use option isabelle build -o document_output=output to see the
result in the "output" directory relative to the session.)

Whenever the update of the Isabelle document preparation system to
HTML/CSS/JS happens, it will interpret these special sequences in the
same manner, i.e. as some HTML non-breaking space.

In source text you should refrain from using Unicode space variations:
it is just too confusing / fragile / non-portable.


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