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



Am Montag, den 15.07.2019, 19:42 +0200 schrieb Makarius:
> 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.

So the backslash–tilde combination is not that Markdown extension that
means a no-break space but the good old LaTeX command. Well, as a LaTeX
command it only means an ordinary space; so for getting a no-break space
I should use the tilde then.

All the best,
Wolfgang





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