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

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?

All the best,

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