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

Dear Chris,

I also watch the theories panel, but I cannot click in the theories panel to take me to the location of the error. For that I need the bar of the main text area.


On 04/02/16 09:55, Christian Sternagel wrote:
It doesn't answer your question, but I usually observe the "Theory"
panel while loading big theories (I think errors are marked there as
soon as they "happen").



On 02/04/2016 08:49 AM, 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.