On Fri, 5 Jul 2013, Makarius wrote:
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.
I was actually expecting some trivial patching of Proof General to be
required for this reform, but checking the elisp sources now, it looks
like nothing is required: there are only some menu and keyboard shortcuts
for these control symbols (excluding \<^isup>), but no specific treatment
of \<^isub> or \<^isup> for identifier regexps, as far as I can see in
5min looking.
So people stuck with PG 3.7.1.1 or an older 4.x version can remain so.
If tiny patches of PG will be required nonetheless, I volunteer to do them
in its repository, and consider applying them the latest official release
as well. Of course, PG needs to retain its support for old Isabelle
releases anyway; it is up to the user to type different sequences of
ESCAPE-META-ALT-CONTROL-SHIFT to get this or that version of subscripts.
Note that current PG 4.2 will be superseded by the coming 4.3 release
soon, but I am merely an observer on its mailing list.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
