[isabelle-dev] Subscripts within identifiers
makarius at sketis.net
Tue Jul 2 18:00:45 CEST 2013
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
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.
More information about the isabelle-dev