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 http://isabelle.in.tum.de/dist/library/HOL/ex/Hebrew.html

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?


	Makarius


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