On 08/08/2013, at 9:18 PM, Makarius makar...@sketis.net wrote:
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
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
On Sat, 13 Jul 2013, Alexander Krauss wrote:
On 07/10/2013 07:25 PM, Makarius wrote:
Even simpler would be to invent a name for some variant of \omega that
is not considered a letter, and use that with \^sup as before. That
would be analogous to \epsilon vs. \some.
Does the mapping from
On Sat, 13 Jul 2013, Tjark Weber wrote:
On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote:
How would Omega Algebras fare with notation A\^sup\infinity instead
of A\^sup\omega?
Worse. Of course, a name is just that, but for clarity and convenience,
it is nice to be able to call things in
On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote:
How would Omega Algebras fare with notation A\^sup\infinity instead
of A\^sup\omega?
Worse. Of course, a name is just that, but for clarity and convenience,
it is nice to be able to call things in Isabelle what they are called
in the
On 07/10/2013 07:25 PM, Makarius wrote:
Even simpler would be to invent a name for some variant of \omega that
is not considered a letter, and use that with \^sup as before. That
would be analogous to \epsilon vs. \some.
Does the mapping from Isabelle symbols to Unicode code points have to
On Wed, 10 Jul 2013, Makarius wrote:
So the reformed identifier syntax is like this:
LETTER = A .. Z a .. Z \alpha ... \A ... \a ... etc.
DIGIT = 0 .. 9
LETDIG = LETTER | DIGIT | _ | '
CONTROL = \^sub | \^sup
IDENTIFIER = LETTER ( CONTROL? LETDIG )*
Isabelle/2077168aa8f7 already
On Wed, 10 Jul 2013, Makarius wrote:
So the reformed identifier syntax is like this:
LETTER = A .. Z a .. Z \alpha ... \A ... \a ... etc.
DIGIT = 0 .. 9
LETDIG = LETTER | DIGIT | _ | '
CONTROL = \^sub | \^sup
IDENTIFIER = LETTER ( CONTROL? LETDIG )*
These changes are most just obscure
This is an update of this important thread.
It turned out that the symmetric version where both \^sub and \^sup
are allowed in the liberal part of identifiers works, with minimal impact
on applications of the known universe.
So the reformed identifier syntax is like this:
LETTER = A .. Z
Am 10/07/2013 16:54, schrieb Makarius:
That is an instance of \^supLETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation by
using \^bsup \^esup which looks almost the same in Latex, but is a bit
awkward in Isabelle/jEdit.
Why
On Wed, 10 Jul 2013, Tobias Nipkow wrote:
Am 10/07/2013 16:54, schrieb Makarius:
That is an instance of \^supLETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation by
using \^bsup \^esup which looks almost the same in Latex, but
On Tue, 2 Jul 2013, Gerwin Klein wrote:
I think we should allow
IDENTIFIER = (SUBSCRIPT LETDIG)? LETTER ( SUBSCRIPT? LETDIG )*
i.e. allow a subscript at the beginning of an identifier. This is
probably not used much (or at all) currently, but I've seen this plenty
of times in maths texts.
On Tue, 2 Jul 2013, Gerwin Klein wrote:
I'm less sure about the distinction between sub and sup. I can see it
mostly aligns with current usage patterns, but I find this distinction
even more confusing.
There are two aspects here: (1) common understanding of users and (2)
technical
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
Am 05/07/2013 14:08, schrieb Makarius:
On Tue, 2 Jul 2013, Gerwin Klein wrote:
I'm less sure about the distinction between sub and sup. I can see it mostly
aligns with current usage patterns, but I find this distinction even more
confusing.
There are two aspects here: (1) common
This issue is so old that hardly anybody remembers that it is an issue:
using subscripts within identifiers without special precautions.
Historically, I was the first to use subscripts in identifiers in my
doctoral thesis -- with some perl script over the generated latex sources
for proper
On 02.07.2013 13:15, Makarius wrote:
After 10 years we actually have a chance to stop such jokes about
identifiers starting or ending with control symbols, or control
symbols getting out of sync, and especially the confusion about which
of the two subscript controls is what.
Nice!
What do
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
On 02.07.2013 18:00, Makarius wrote:
* 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
19 matches
Mail list logo
