Email Gateway (Aug 22 2022 at 17:12): Email Gateway (Aug 22 2022 at 17:12):From: Rafal Kolanski <xs@xaph.net>
Hello,
In our group, we use a jEdit macro that jumps to the first error of a
theory file. In large theory files, it's hard to click on the right spot
on the theory overview, and it's much easier to twitch some key
combination the moment you see red in the progress bar.
Larry is a big fan, and always pokes me when some update causes
breakage. He suggested I disseminate it more widely.
The attached version is updated to work on Isabelle 2017 and the dev
version as of about a week ago. Place in ~/.isabelle/jedit/macros then
do Macros->Rescan Macros, or restart jEdit.
We typically bind it to a key combination and have a hard time living
without it.
Let me know if you have any questions.
Sincerely,
Rafal Kolanski
goto-error.bsh
Email Gateway (Aug 22 2022 at 17:12):From: Dominique Unruh <unruh@ut.ee>
Brilliant!
I would love to see this (or something similar) integrated in the
Isabelle/jEdit distribution.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:46):From: Makarius <makarius@sketis.net>
I still did not find time to look at it, and it is unlikely that I will
do before the Isabelle2018 release. I've heard about it for the very
first time some months ago, when it suddenly popped it in a private mail
thread.
Makarius
Email Gateway (Aug 22 2022 at 17:46):From: Gerwin.Klein@data61.csiro.au
On 6 Jul 2018, at 22:25, Makarius <makarius@sketis.net> wrote:
On 31/05/18 01:38, Rafal Kolanski wrote:
In our group, we use a jEdit macro that jumps to the first error of a
theory file. In large theory files, it's hard to click on the right spot
on the theory overview, and it's much easier to twitch some key
combination the moment you see red in the progress bar.Larry is a big fan, and always pokes me when some update causes
breakage. He suggested I disseminate it more widely.I still did not find time to look at it, and it is unlikely that I will
do before the Isabelle2018 release.
Happy to help with that if that if I can do anything useful.
I've heard about it for the very
first time some months ago, when it suddenly popped it in a private mail
thread.
I’m pretty sure that we’ve pointed to this script multiple times in the last few years, e.g. Raf’s message from 7 Feb 2016 on isabelle-users.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 17:46):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s extremely convenient, especially for maintenance. I use it constantly.
--lcp
Email Gateway (Aug 22 2022 at 17:46):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
I would love to see it in next Isabelle distribution. It is extremly
important for someone like me who has to do porting of large theories
related to a very deep and complex formalism.
Another feature that I would like to see in future is something that allows
searching terms in proof goals in the output.
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 17:46):From: Dominique Unruh <unruh@ut.ee>
I made a small variant of the script. When no error is found, it jumps to
the end of the buffer (instead of a popup) which triggers the processing of
the rest of the proof text in the file, allowing me to find further errors
and then invoking the script again. (So when pressing the hotkey twice, I
get to the next error even if it wasn't processed yet.) This saves a few
key presses. It's certainly a matter of taste whether this is better or
worse than the original, but I am attaching it for those who prefer this
mechanism.
Best wishes,
Dominique.
goto-error.bsh
Email Gateway (Aug 23 2022 at 08:31):From: Makarius <makarius@sketis.net>
Two release cycles later I've now had a look at it: the implementation in
BeanShell makes it all very non-standard and hard to understand from the
normal Isabelle/Scala perspective: it is surprising that BeanShell can do this
at all.
After further studies of the sitation I have now implemented various
"Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions"
for Isabelle2020, see also
https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions
That will be part of Isabelle2010-RC1 to be published within a few hours.
Makarius
Email Gateway (Aug 23 2022 at 08:39):From: Makarius <makarius@sketis.net>
On 2 Mar 2020, 15:05 +0000, Makarius <makarius@sketis.net>, wrote:
After further studies of the sitation I have now implemented various
"Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions"
for Isabelle2020, see alsoThat will be part of Isabelle2010-RC1 to be published within a few hours.
On 02/03/2020 16:45, Lawrence Paulson wrote:
These will be very useful, thanks!
But what do you mean by CS?
That is standard jEdit terminology: it means CONTROL-SHIFT on Linux or
Windows, and COMMAND-SHIFT on macOS.
Makarius
Email Gateway (Aug 23 2022 at 08:42):From: Makarius <makarius@sketis.net>
This is all getting a bit complicated, and we are very close to the final release.
I have now reverted the last minute change to include "bad" markup into the
notion of errors, see
https://isabelle.sketis.net/repos/isabelle-release/rev/76b739c0bedd
If you want to follow these changes before the next official release
candidate, you need to work from that repository. See also
https://isabelle.sketis.net/repos/isabelle-release/file/tip/README_REPOSITORY
using the correct base URL for hg clone.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC