makarius at sketis.net
Tue Sep 2 17:44:11 CEST 2008
On Tue, 2 Sep 2008, David Aspinall wrote:
> This is already supported in the X-Symbol replacement in the CVS version of
> Proof General, by the way, although Isabelle's lexer currently only allows
> syntax like \<caret1> and \<caret2>.
The \<symbol> notation is more fundamental, below lexing even. It is
actually fashioned after Java's \uDDDD for UTF-16 chars, but we do not
depend on unicode encoding variants of course.
You can achieve the above "name space effect" of symbols already via
something like \<caret_funpow>, which is presently unused because LaTeX
output is a bit strange (as for \<caret1>). This means \<foo_bar> and
\<foo42> are both unlikely to be used already for something else.
There is also a more compositional way to produce symbol variants:
\<^control>\<symbol>. Here nothing needs to be changed in Isabelle, only
the UI needs to provide sane input methods and proper display (without the
flashing of x-symbol for \<^sub> for example).
More information about the isabelle-dev