[isabelle-dev] Subscripts within identifiers
nipkow at in.tum.de
Fri Jul 5 15:38:09 CEST 2013
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
> 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:
> 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".
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.
>> 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
> 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.)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev