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