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

On Thu, 4 Feb 2016, Andreas Lochbihler wrote:

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).

This is indeed a bit odd. The text overview column has been reworked significantly for Isabelle2016, but a few fine points still need to be polished further.

Presently there is
to improve this: less CPU requirements, more reactivity.

The next Isabelle2016-RC will be published officially within a few days.


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