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