Email Gateway (Aug 23 2022 at 08:37): Email Gateway (Aug 23 2022 at 08:37):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Say I have the following declaration of a notation:
notation False (‹†' ‡›)
Strangely, neither the term ‹† ‡› not the term ‹†‡› is accepted
afterwards. If I remove the apostrophe from the mixfix declaration, both
terms are accepted.
What’s the reason for this behavior? In my opinion, whether the
apostrophe is present or absent shouldn’t make any difference for
parsing.
I’m using Isabelle2019.
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:39):From: Makarius <makarius@sketis.net>
I don't understand the "opinion". Is this based on the documentation (isar-ref
manual section 8.2.1)?
A single quote escapes the next meta character, but a space is not allowed
here. So this is an undefined case, and there should probably be a better
error instead of just documentation.
Maybe you actually intended to do the following:
notation False (‹†()‡›)
Now you get two separate delimiters, and the whitespace becomes optional for
input.
Makarius
Email Gateway (Aug 23 2022 at 08:39):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Am Donnerstag, den 12.03.2020, 22:10 +0100 schrieb Makarius:
On 07/03/2020 02:20, Wolfgang Jeltsch wrote:
Say I have the following declaration of a notation:
notation False (‹†' ‡›)
Strangely, neither the term ‹† ‡› not the term ‹†‡› is accepted
afterwards. If I remove the apostrophe from the mixfix declaration,
both terms are accepted.What’s the reason for this behavior? In my opinion, whether the
apostrophe is present or absent shouldn’t make any difference for
parsing.I don't understand the "opinion". Is this based on the documentation
(isar-ref manual section 8.2.1)?
Yes. It says:
A single quote followed by a blank separates delimiters, without
affecting printing, but input tokens may have additional white space
here.
Maybe you actually intended to do the following:
notation False (‹†()‡›)
Now you get two separate delimiters, and the whitespace becomes
optional for input.
A had been considering this. However, I wasn’t sure about unintended
consequences. The parentheses would introduce an empty “pretty-printing
block”. Would this mean the pretty printer could insert a line break
there?
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:40):From: Makarius <makarius@sketis.net>
On 13/03/2020 00:56, Wolfgang Jeltsch wrote:
Am Donnerstag, den 12.03.2020, 22:10 +0100 schrieb Makarius:
On 07/03/2020 02:20, Wolfgang Jeltsch wrote:
Say I have the following declaration of a notation:
notation False (‹†' ‡›)
Strangely, neither the term ‹† ‡› not the term ‹†‡› is accepted
afterwards. If I remove the apostrophe from the mixfix declaration,
both terms are accepted.What’s the reason for this behavior? In my opinion, whether the
apostrophe is present or absent shouldn’t make any difference for
parsing.I don't understand the "opinion". Is this based on the documentation
(isar-ref manual section 8.2.1)?Yes. It says:
A single quote followed by a blank separates delimiters, without
affecting printing, but input tokens may have additional white space
here.
You are right. This text has been there since Feb-1995 with implementation of
the feature, but it was never used and accidentally destroyed in Mar-1998. The
relevant changesets are as follows (by myself!):
https://isabelle-dev.sketis.net/rISABELLE55754d6d399c
https://isabelle-dev.sketis.net/rISABELLEbe8a8d60d962
The latter talks about "baroque chars" in the wrong spelling. The concept is
now known as "Isabelle symbols" and has served us very well since its
introduction in 1998.
Maybe you actually intended to do the following:
notation False (‹†()‡›)
Now you get two separate delimiters, and the whitespace becomes
optional for input.A had been considering this. However, I wasn’t sure about unintended
consequences. The parentheses would introduce an empty “pretty-printing
block”. Would this mean the pretty printer could insert a line break
there?
The empty-block technique has been standard for more than 20 years. There is
no problem to insert such a dummy into the pretty tree: breaks cannot happen
unless you say so (via "/" in the mixfix template).
Nonetheless, I have now made another change for Isabelle2020 to reactivate
this ancient detail. See now:
https://isabelle-dev.sketis.net/rISABELLEb0b16088ccf2
As a consequence, a trailing single quote is no longer included in delimiter
by accident, but needs to be escaped as documented. E.g. see:
https://isabelle-dev.sketis.net/rISABELLEd350aabace23
Overall these single quotes are a bit odd, stemming from a time of ASCII-art.
After the Isabelle2020 release, I will revisit that eventually and provide a
more contemporary solution, e.g. like this via the \<^verbatim> control symbol:
notation False (‹▩‹†›▩‹‡››)
Thus we could even discontinue the single quote as a mixfix meta character
later on.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC