Email Gateway (Oct 10 2024 at 18:17): Email Gateway (Oct 10 2024 at 18:17):From: Makarius <makarius@sketis.net>
Are there any remaining uses of show_brackets?
Here is historical proof for this feature from many decades ago:
changeset: 504:a4f09493d929
user: nipkow
date: Tue Aug 02 09:07:10 1994 +0200
files: src/Pure/Syntax/printer.ML
description:
added flag show_brackets for printinmg fully bracketed terms.
changeset: 508:d8b6999ca364
user: lcp
date: Thu Aug 04 11:51:30 1994 +0200
files: doc-src/Ref/introduction.tex
description:
addition of show_brackets
The documentation in d8b6999ca364 says: "show_brackets makes Isabelle show
full bracketing. This reveals the grouping of infix operators."
We have that already via PIDE markup for pretty-blocks, see also
Isabelle/87f173836d56 --- and it works more accurately, too.
So if there are no further uses of it, I will remove it shortly before the
Isabelle2025 release process starts (Jan-2025).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 18:27):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes – for anyone who wants their proof states to be legible. I always recommend it to students.
It’s exactly the same principle as having [_,_,_] for lists instead of _::_::_::nil.
Larry
On 10 Oct 2024, at 19:16, Makarius <makarius@sketis.net> wrote:
Are there any remaining uses of show_brackets?
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 18:52):From: Makarius <makarius@sketis.net>
On 10/10/2024 20:26, Lawrence Paulson wrote:
Yes – for anyone who wants their proof states to be legible. I always recommend it to students.
I don't understand what you mean by "legible". How is the following example
legible?
declare [[show_brackets]]
lemma ‹∀x y. P x y ⟶ Q y x›
goal (1 subgoal):
1. (∀(x y). ((P x y) ⟶ (Q y x)))
The parentheses for the variable bindings are even wrong in the sense of the
formal syntax.
It’s exactly the same principle as having [_,_,_] for lists instead of _::_::_::nil.
I don't understand that either. Can you explain that, please?
If I would understand the principle, I could say if cane be done via PIDE
rendering instead of occasionally bad parentheses.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 19:19):From: Peter Lammich <lammich@in.tum.de>
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 20:49):From: Lawrence Paulson <lp15@cam.ac.uk>
Oh, that one. I quite forgot it was there. But it’s occasionally useful when you aren’t sure about operator precedences. Is it hard to support?
Larry
On 10 Oct 2024, at 19:51, Makarius <makarius@sketis.net> wrote:
I don't understand what you mean by "legible". How is the following example legible?
declare [[show_brackets]]
lemma ‹∀x y. P x y ⟶ Q y x›goal (1 subgoal):
1. (∀(x y). ((P x y) ⟶ (Q y x)))
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 10 2024 at 20:49):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes – exactly and especially when implications are nested.
Larry
On 10 Oct 2024, at 20:19, Peter Lammich <lammich@in.tum.de> wrote:
I think here's a confusion between the attribute that shows all parentheses and the print mode that switches printing of premises from a==>b==>... to [|a;b;...|]==>
Please do not remove the latter, as it has many users. It makes long subgoals more readable, as you don't have to find the last==> to interpret the goal.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 08:14):From: Makarius <makarius@sketis.net>
On 10 Oct 2024, at 19:51, Makarius <makarius@sketis.net> wrote:
I don't understand what you mean by "legible". How is the following
example legible?declare [[show_brackets]]
lemma ‹∀x y. P x y ⟶ Q y x›goal (1 subgoal):
1. (∀(x y). ((P x y) ⟶ (Q y x)))
On 10/10/2024 22:48, Lawrence Paulson wrote:
Oh, that one. I quite forgot it was there. But it’s occasionally useful when you aren’t sure about operator precedences. Is it hard to support?
It is a totally adhoc feature from 30 years ago, and incorrect in certain
situations.
Can you try if the new mixfix markup works sufficiently well to replace this
idea? The new scheme works for parsed input source and pretty-printed output.
You just C-hover over the text, and get feedback about its inner-syntax structure.
People might call that a "parse tree", but it is better than a raw parse tree
(which contains a lot of irrelevant information).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 08:16):From: Makarius <makarius@sketis.net>
On 10/10/2024 21:19, Peter Lammich wrote:
I think here's a confusion between the attribute that shows all parentheses
and the print mode that switches printing of premises from a==>b==>... to
[|a;b;...|]==>Please do not remove the latter, as it has many users. It makes long subgoals
more readable, as you don't have to find the last==> to interpret the goal.
That is unrelated to the current thread. The time to ask about its "remaining
uses" it not there yet, but it will come when the proof state output has been
warped 20 yeards foreward. (That is not going to happen for Isabelle2025.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 08:45):From: Peter Lammich <lammich@in.tum.de>
On 11/10/2024 10:13, Makarius wrote:
On 10 Oct 2024, at 19:51, Makarius <makarius@sketis.net> wrote:
I don't understand what you mean by "legible". How is the following
example legible?declare [[show_brackets]]
lemma ‹∀x y. P x y ⟶ Q y x›goal (1 subgoal):
1. (∀(x y). ((P x y) ⟶ (Q y x)))On 10/10/2024 22:48, Lawrence Paulson wrote:
Oh, that one. I quite forgot it was there. But it’s occasionally
useful when you aren’t sure about operator precedences. Is it hard to
support?
If I'm unsure about operator precedence, I usually go the other way
round: I manually add some parentheses, and see how/if the
pretty-printed term changes
--
Peter
It is a totally adhoc feature from 30 years ago, and incorrect in
certain situations.Can you try if the new mixfix markup works sufficiently well to
replace this idea? The new scheme works for parsed input source and
pretty-printed output. You just C-hover over the text, and get
feedback about its inner-syntax structure.People might call that a "parse tree", but it is better than a raw
parse tree (which contains a lot of irrelevant information).Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 11:41):From: Lawrence Paulson <lp15@cam.ac.uk>
I tried it on a set comprehension and got
notation: mixfix "set comprehension”
This is pretty useful, because in the past there was no way to examine non-trivial syntax constructions, which in some cases were a complete mystery.
If it's not too difficult, could it be possible to jump to the original definition?
Larry
On 11 Oct 2024, at 09:13, Makarius <makarius@sketis.net> wrote:
Can you try if the new mixfix markup works sufficiently well to replace this idea? The new scheme works for parsed input source and pretty-printed output. You just C-hover over the text, and get feedback about its inner-syntax structure.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 11:49):From: Makarius <makarius@sketis.net>
On 11/10/2024 13:41, Lawrence Paulson wrote:
I tried it on a set comprehension and got
notation: mixfix "set comprehension”
This is pretty useful, because in the past there was no way to examine non-trivial syntax constructions, which in some cases were a complete mystery.
If it's not too difficult, could it be possible to jump to the original definition?
That is also possible: I've actually had that before setting out for all this
"notation=..." markup. It is merely a matter of adding 'syntax_consts'
declarations, like I've always done for "notation=binder" to imitate regular
'binder' declarations. You can see that e.g. in prop "∀x∈A. P x"
A minor disadvantage: the present PIDE rendering sometimes hides markup that
is stacked up too ambitiously, and there is no whitespace between tokens to
hover over it.
So I will keep this on the TODO list to think about further ...
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 11 2024 at 11:52):From: Makarius <makarius@sketis.net>
On 11/10/2024 10:45, Peter Lammich wrote:
On 10/10/2024 22:48, Lawrence Paulson wrote:
Oh, that one. I quite forgot it was there. But it’s occasionally useful
when you aren’t sure about operator precedences. Is it hard to support?If I'm unsure about operator precedence, I usually go the other way round: I
manually add some parentheses, and see how/if the pretty-printed term changes
So now is a good oppurtinity to try the new markup scheme of
Isabelle/87f173836d56.
It can save a lot of time, because things don't have to be printed to see the
term structure.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC