Re: [isabelle] Isabelle2016-RC3: delayed updated of error bar in main text area



Hi Andreas,

We have large proofs too and often find ourselves "looking for the red
bit" while no red bit appears in the text overview. Additionally,
clicking with the mouse isn't super accurate. Please consider trying out
my hack to jump to the first error in the current theory file:

https://github.com/seL4/l4v/blob/master/misc/jedit/macros/goto-error.bsh

I have it bound to ctrl+shift+e and use it all the time.

Hopefully this will help a bit.

Raf.

On 04/02/16 18:49, Andreas Lochbihler wrote:
> Dear Makarius,
> 
> I've noticed with Isabelle2016-RC3 that the bar on the right hand side
> of the main text area (in which errors are marked with red lines,
> warnings with yellow ones, and unprocessed parts in light red) seems not
> to be updated synchronously with the processing of the theory file.
> 
> When I change something a large theory file (more than 8000 lines)
> somewhere in the beginning, I then normally jump to the end of the file
> to have it reprocessed. As soon as an error occurs (indicated by a red
> bar in the theory panel), I then would like to click on the red line in
> the bar on the right of the main text area to immediately jump to the
> error and make the necessary adaptations. Unfortunately, in
> Isabelle2016-RC3, the bar does not seem to get updated as regularly as
> in Isabelle2015, the update only happens if processing approaches the
> end of my theory (which can take a while). If there is an error fairly
> at the beginning, then after having fixed this, I again have to wait
> until most of it is processed until I find the next error. Is there some
> configuration to have the bar updated more frequently?
> 
> Best,
> Andreas
> 




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