[isabelle-dev] Subscripts within identifiers

[Makarius]

On Tue, 2 Jul 2013, Lars Noschinski wrote:

> What do you mean by "getting out of sync" in contrast to "starting/ending 
> with control symbols"?

There are just control symbols that do not control regular symbols: any 
sequence of more than one controls, or some control at the end of the 
identifier with whatever follows after it (e.g. blank or quote).

In Isabelle/jEdit there is an auxiliary notion of "controllable" symbols, 
to make a visual sub/superscript only in the "known-good" situations. 
This is why the odd joke about identifiers of 1/2/3 control symbols is 
visually not as bad as in Proof General.


>>  * 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?

I do not understand the LETTER aspect in this question.  The front-ends 
interpret certain control symbols independently of these token syntax 
considerations: \<^sub>1 is rendered accordingly, wherever it occurs.

After collapsing \<^sub> and \<^isub> to just \<^sub>, Isabelle/jEdit 
could retain the Unicode arrow of \<^isub> without the subscripting 
effect, to make a decent lagacy view.  (It could also add some "bad" 
markup on top of that to remind the user of old things being changed.)


>>  * 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.

That example is just about notation.  Mixfix delimiters may use arbitary 
symbols.  One merely needs to watch out for conflicts emerging with the 
built-in syntax of identifiers (and other tokens).

The above looks fine to me.  It would merely come out as 
\<rightarrow>\<^sup>*\<index>.  The \<index> part then uses 
\<^bsub>..\<^esub> as usual.  (Many years ago there would have been a 
conflict with \<^sub>DIGIT for the index slot, but that has disappeared 
some years ago.)


>>  * 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?

Empirically, there was never substantial use of \<^isup> apart from 
extreme boundary cases.  In such cases it is often possible to use 
explicit mixfix notation, as I have occasionally done for Lebesgue 
integral as notation.

Presently, the only use of \<^isup> in the repository is in 
src/Doc/Tutorial, warning the user that \<^isup> superscript is not to be 
confused with \<^sup> notation.


This empirical asymmetry of \<^sup> for notation vs. \<^sub> for 
identifiers is practically important.  Otherwise the collapse would not be 
possible.

I could dig up some changesets that introduce \<^sub> in identifiers, 
later noticing a clash and making the copy \<^isub>, then realizing that 
this admits \<^isup> in identifiers without a clash with existing \<^sup> 
practice for notation.


>>  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? ]

That is a different fine point: the lexical syntax admits trailing "_", 
but identifiers with that are rejected later on (as "internal" ones). 
Attempting to clarify that syntax turned out as infeasible so far, which 
is one of the reasons why I have abandoned more ambitious structuring of 
identifiers with "_" as formal separator.


 	Makarius