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



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.