Re: [isabelle] Updated goto-error script for Isabelle (jumps to first error in theory file)



Brilliant!

I would love to see this (or something similar) integrated in the
Isabelle/jEdit distribution.

Best wishes,
Dominique.


On 30 May 2018 at 19:38, Rafal Kolanski <xs at xaph.net> wrote:

> 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
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.