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


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

Best wishes,

On 30 May 2018 at 19:38, Rafal Kolanski <xs at> 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.