On 02.07.2013 13:15, Makarius wrote:
> After 10 years we actually have a chance to stop such jokes about
> identifiers starting or ending with control symbols, or control
> symbols getting out of sync, and especially the confusion about which
> of the two subscript controls is what.
Nice!
What do you mean by "getting out of sync" in contrast to
"starting/ending with control symbols"?
* There is just one \<^sub> and \<^sup> control symbol to that effect;
\<^isub> and \<^isup> remain within the infinite collection of
Isabelle symbols without any special meaning.
I.e., in the notation below they are not are LETTERs anymore and the
then-current IDEs will stop rendering them as sub-/superscripts?
* Superscript is for explicit notation, e.g. "x\<^sup>2" for some
operator "_\<^sup>2" applied to term x.
Graph_Theory/Digraph from the AFP defines a constant reachable
with syntax
("_ \<rightarrow>\<^isup>*\<index> _" [100,100] 40)
(this should probably by "infix" instead). Is this going to stay
valid (with \<^isup> replaced by \<^sup>)? It does not quite fit the
scheme you described above.
> * Subscript may get used within identifiers, e.g. "x\<^sub>2" for a
> variable of that name.
This proposal excludes superscripts from occurring in identifiers. Does
this mean that there was no legitimate use of \<isup> at all?
Instead of making \<^sub> a "letter" as was done in Isabelle2003, the
syntax is changed like this:
LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc.
DIGIT = 0 .. 9
LETDIG = LETTER | DIGIT | _ | '
SUBSCRIPT = \<^sub>
IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )*
[ I always assumed the "_" was also excluded from occurring at the end
of a (parsed) identifier? ]
Best regards,
Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
