[isabelle-dev] Subscripts within identifiers

[Lars Noschinski]

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