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

Hi Rafal,

Thanks for the pointer to the macro. This is really useful.


On 07/02/16 13:02, Rafal Kolanski wrote:
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:

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

Hopefully this will help a bit.


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?


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