Re: [isabelle] unicode tokens in isabelle2011+pg4.0

On Wed, 2 Feb 2011, Joachim Breitner wrote:

is there a reason why Isabelle would not accept ∀ synonymously to \<forall> in theory files? This would also be nice for all those unicode-loving folk who occasionally at .thy files directly (e.g. doing some mass-substitution with vim, or looking at diffs).

The deeper reason is that unicode is neither uniform nor universal. By keeping encodings and assumptions about availability of glyphs out of the Isabelle sources, they can be used with plain text tools as described above, because it is plain ASCII by default.

The situation is different for front-ends based on Isabelle/Scala (such as Isabelle/jEdit). There is a default mapping between Isabelle symbols and JVM-based unicode, which is used here as a poort-mans rendering engine for mathematical symbols. Thus \<forall> vs. its corresponding unicode glyph are treated interchangeably by the user interface. This works well under the assumption that there is no conflict with independent unicodes in user sources.


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