[isabelle-dev] Subscripts within identifiers

[Makarius]

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