Email Gateway (Aug 19 2022 at 14:14): Email Gateway (Aug 19 2022 at 14:14):From: Joachim Breitner <breitner@kit.edu>
Dear List,
I am currently doing something tedious that I find myself doing often:
After having finished a theory I polish it up, including adding nicely
looking notation. And then I begin going through my theory, putting the
cursor on any lemma declaration or "have" and copy the nicely printed
output from the output buffer to the editor buffer.
For definitions and "assumes", I first have to call "thm foo_def" or
"thm assms" to get hold of that display.
It would be great if that process was made easier, maybe by a button in
the popup that is (sometimes?) visible when I hover over such a
statement, or even better a keyboard combination (similar to how jEdit
will format a paragraph when I use "C-e f").
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 14:14):From: Tobias Nipkow <nipkow@in.tum.de>
Although I do not do this editing that Joachim describes, I also sometimes
wish that defnitions and lemmas would print the proposition to see what it
looks like.
Tobias
Email Gateway (Aug 19 2022 at 14:25):From: Makarius <makarius@sketis.net>
There is a long and thorny history behind certain variations of printing
of "state" or "results" -- in TTY mode, Proof General 2.x, 3.x, 4.x, even
Isabelle/jEdit with its 5 years. I have looked a bit through all that
once again, and there is a good chance that it will be more smooth in the
coming release -- not every detail from the past needs to be retained
today.
When the Isabelle2014-RC phase starts, presumably in July, you should take
the opportunity to make a serious test of the many new things that have
accumulated.
Makarius
Email Gateway (Aug 19 2022 at 14:32):From: Julian Brunner <julianbrunner@gmail.com>
On Wed, Apr 30, 2014 at 11:54 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:
Although I do not do this editing that Joachim describes, I also sometimes
wish that defnitions and lemmas would print the proposition to see what it
looks like.
I second this. Definitions and the final proof steps of theorem
statements don't have any print output yet, so there's an unused
opportunity to provide information. The final proof steps of have,
show and obtain statements in isar proofs already do this, too.
Tobias
On 30/04/2014 11:16, Joachim Breitner wrote:
Dear List,
I am currently doing something tedious that I find myself doing often:
After having finished a theory I polish it up, including adding nicely
looking notation. And then I begin going through my theory, putting the
cursor on any lemma declaration or "have" and copy the nicely printed
output from the output buffer to the editor buffer.For definitions and "assumes", I first have to call "thm foo_def" or "thm
assms" to get hold of that display.It would be great if that process was made easier, maybe by a button in the
popup that is (sometimes?) visible when I hover over such a statement, or
even better a keyboard combination (similar to how jEdit will format a
paragraph when I use "C-e f").Thanks, Joachim
Last updated: Nov 21 2024 at 12:39 UTC