[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Fri Jul 5 14:43:05 CEST 2013
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
So people stuck with PG 188.8.131.52 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.
More information about the isabelle-dev