[isabelle-dev] Subscripts within identifiers

[Makarius]

This thread is still awaiting its conclusion ...

To get it away from its almost 0 level of potential energy, I had already 
collected some impressions from seasoned users of Isabelle notation at the 
ITP conference. Moreover, I have looked through the Fortress Language 
specification again: they have some sophistication to render identifiers 
with subscripts, but superscripts are for certain postfix operators, 
including the special \<^sup>T for matrix transposition.

Together with our \<^sub>\<omega> this reconfirms my initial impression 
that it is better to have the asymmetry of \<^sub> for identifiers vs. 
\<^sup> for notation.  As a consequence, \<twosuperior> also becomes 
obsolete; \<onesuperior> and \<threesuperior> were never used in practice, 
and the other superscripted 4..9 from unicode never assigned in our 
default symbol interpretation (they are missing in the IsabelleText font).


This is the refined proposal according to lib/scripts/update_sub_sup in 
Isabelle/0ea2b657eb42:

   * The identifier syntax is the minimal extension of classic ML from
     the very start of this thread:

      LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc.
      DIGIT = 0 .. 9
      LETDIG = LETTER | DIGIT | _ | '
      SUBSCRIPT = \<^sub>

      IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )*

    * Subscript may get used within identifiers, e.g. "x\<^sub>2" for a
      variable of that name.

    * Superscript is for explicit notation, e.g. "x\<^sup>2" for some
      operator "_\<^sup>2" applied to term x.

    * \<twosuperior> is expanded to \<^sup>2 in the Isabelle/HOL library
      and AFP -- there are relatively few occurrences of it.

    * The following Isabelle symbols loose their default assignment and
      special interpretation: \<^isub> \<^isup> \<onesuperior>
      \<twosuperior> \<threesuperior>

The "isabelle update_sub_sup" tool should work for most users without 
further ado.  It is also possible to provide some legacy_isub_isup flag in 
Isabelle/ML to help the transition: the prover then accepts old \<^isub> 
and \<^isup> in addition to the new \<^sup> for SUBSCRIPT above (it is off 
by default).

So everything is ready to push the red button ...


Once this is settled, I will make a second round to ensure that the 
slightly awkward \<^bsub>...\<^esub> is not used in literal tokens of 
notation unnecessarily.  A block of symbols is better sub- or 
superscripted by preceeding each symbol with a separate control symbol. 
Isabelle/jEdit supports this smoothly, using the normal buttons in the 
Symbols panel or corresponding keyboard shortcuts, but with an active text 
selection.  (This is still not a rich-text editor, since these "text 
styles" cannot be nested.)


 	Makarius