[isabelle-dev] Subscripts within identifiers

[Tobias Nipkow]

Am 05/07/2013 14:08, schrieb 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.

True.

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

I think this is not a good example. If you write "x\<isup>2" now it is an
identifier and if you write "x\<^sup>2" it is illegal. If you refer to
"x\<twosuperior>", that is a hack (but you could still write it).

You probably mean things like R\<^sup>*, and we would have to write
R\<^bsup>*<^esup> instead, which is indeed not appealing.

Tobias

> 
>> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev