Re: [isabelle] Document processing with XeLaTeX and unicode symbols
On Mon, 15 Oct 2012, Makarius wrote:
On Sat, 13 Oct 2012, Lars Hupel wrote:
(*) side note: xelatex is able to process Unicode tokens, so it would be
fine if the .thy or .tex file simply contained '»' and '«'.
This sounds like you are still optimistic about Unicode in general.
For me a sentence with "able to process" and "Unicode" is an Oxymoron,
after several years of struggling with this constantly changing
standard. There are so many things that can go wrong with Unicode.
Just for fun another unicode joke: see
The example mixes formal and informal use of Unicode in an optimistic way
-- I made this when Emacs22 started to support it some years ago.
If you look at the last lemma with *correct* rendering of Unicode
according to the standard (e.g. in Firefox), you will be surprised about
the swap of the digits "135" with the "he" letter wrt. to the "=" sign.
Luckily neither Emacs nor jEdit conform to the Unicode standard of
rendering the mix of left-to-right and right-to-left text.
How does xelatex handle this example? Does it render Unicode according to
the standard here and thus produce logical non-sense?
This archive was generated by a fusion of
Pipermail (Mailman edition) and