[isabelle-dev] Subscripts within identifiers

[Makarius]

On Tue, 2 Jul 2013, Gerwin Klein wrote:

> I'm less sure about the distinction between sub and sup. I can see it 
> mostly aligns with current usage patterns, but I find this distinction 
> even more confusing.

There are two aspects here: (1) common understanding of users and (2) 
technical side-conditions. For me, both are speaking for that distinction: 
sub for identifiers, sup for notation.  E.g. consider the example again:

   x\<^sub>2
   x\<^sup>2

When I seen "x subscripted 2" it is by default an identifier, but "x 
superscripted 2" is x-squared.

And technically, treating both the same would make most of our syntax 
break down. You would have to put a space for x-squared: "x \<^sup>2".


> Maybe that's just me and it's worth it if we can eliminate the isub/sub 
> dimension. I can live with either, so I'll leave it to others to argue 
> about it.

This is how things came along in 2003:

changeset:   14234:9590df3c5f2a
user:        kleing
date:        Wed Oct 15 07:03:43 2003 +0200
files:       NEWS lib/texinputs/isabelle.sty src/Pure/General/symbol.ML
description:
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
conflict with locale subscript syntax)

So the seperate pair of control symbols (motivated by avoid the clash) had 
the secondary effect of allowing \<^isub> within identifiers as well.

Maybe you remember more details yourself from back then.  There are more 
changesets involved for the whole story, though.


Just empirically, the \<^isup> notation hardly ever showed up in practice 
in the last 10 years.  The reason for that might be as lame as lack of 
keyboard shortcuts in certain versions of Proof General, IIRC.

BTW, Isabelle/jEdit has quite nice keyboard and GUI tool support for 
sub/superscripts, but just one set of them, not two.  Visial rendering is 
also better than in any Emacs version we've had in 15 years.  And I must 
admit myself that learning new special tricks is getting difficult at my 
age, so it is better to invest efforts to keep things as simple as 
possible.  (Younger guys learning the system afresh will also benefit from 
the simplification.)


 	Makarius