On Tue, 2 Jul 2013, Lars Noschinski wrote:
What do you mean by "getting out of sync" in contrast to "starting/ending
with control symbols"?
There are just control symbols that do not control regular symbols: any
sequence of more than one controls, or some control at the end of the
identifier with whatever follows after it (e.g. blank or quote).
In Isabelle/jEdit there is an auxiliary notion of "controllable" symbols,
to make a visual sub/superscript only in the "known-good" situations.
This is why the odd joke about identifiers of 1/2/3 control symbols is
visually not as bad as in Proof General.
* There is just one \<^sub> and \<^sup> control symbol to that effect;
\<^isub> and \<^isup> remain within the infinite collection of
Isabelle symbols without any special meaning.
I.e., in the notation below they are not are LETTERs anymore and the
then-current IDEs will stop rendering them as sub-/superscripts?
I do not understand the LETTER aspect in this question. The front-ends
interpret certain control symbols independently of these token syntax
considerations: \<^sub>1 is rendered accordingly, wherever it occurs.
After collapsing \<^sub> and \<^isub> to just \<^sub>, Isabelle/jEdit
could retain the Unicode arrow of \<^isub> without the subscripting
effect, to make a decent lagacy view. (It could also add some "bad"
markup on top of that to remind the user of old things being changed.)
* Superscript is for explicit notation, e.g. "x\<^sup>2" for some
operator "_\<^sup>2" applied to term x.
Graph_Theory/Digraph from the AFP defines a constant reachable
with syntax
("_ \<rightarrow>\<^isup>*\<index> _" [100,100] 40)
(this should probably by "infix" instead). Is this going to stay
valid (with \<^isup> replaced by \<^sup>)? It does not quite fit the scheme
you described above.
That example is just about notation. Mixfix delimiters may use arbitary
symbols. One merely needs to watch out for conflicts emerging with the
built-in syntax of identifiers (and other tokens).
The above looks fine to me. It would merely come out as
\<rightarrow>\<^sup>*\<index>. The \<index> part then uses
\<^bsub>..\<^esub> as usual. (Many years ago there would have been a
conflict with \<^sub>DIGIT for the index slot, but that has disappeared
some years ago.)
* Subscript may get used within identifiers, e.g. "x\<^sub>2" for a
variable of that name.
This proposal excludes superscripts from occurring in identifiers. Does this
mean that there was no legitimate use of \<isup> at all?
Empirically, there was never substantial use of \<^isup> apart from
extreme boundary cases. In such cases it is often possible to use
explicit mixfix notation, as I have occasionally done for Lebesgue
integral as notation.
Presently, the only use of \<^isup> in the repository is in
src/Doc/Tutorial, warning the user that \<^isup> superscript is not to be
confused with \<^sup> notation.
This empirical asymmetry of \<^sup> for notation vs. \<^sub> for
identifiers is practically important. Otherwise the collapse would not be
possible.
I could dig up some changesets that introduce \<^sub> in identifiers,
later noticing a clash and making the copy \<^isub>, then realizing that
this admits \<^isup> in identifiers without a clash with existing \<^sup>
practice for notation.
Instead of making \<^sub> a "letter" as was done in Isabelle2003, the
syntax is changed like this:
LETTER = A .. Z a .. Z \<alpha> ... \<A> ... \<a> ... etc.
DIGIT = 0 .. 9
LETDIG = LETTER | DIGIT | _ | '
SUBSCRIPT = \<^sub>
IDENTIFIER = LETTER ( SUBSCRIPT? LETDIG )*
[ I always assumed the "_" was also excluded from occurring at the end
of a (parsed) identifier? ]
That is a different fine point: the lexical syntax admits trailing "_",
but identifiers with that are rejected later on (as "internal" ones).
Attempting to clarify that syntax turned out as infeasible so far, which
is one of the reasons why I have abandoned more ambitious structuring of
identifiers with "_" as formal separator.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
