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

Dear Makarius,

I'll try again after the next RC will have been published and let you know whether things have improved.


On 04/02/16 22:42, Makarius wrote:
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.