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



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

cheers

chris

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?
> 
> Best,
> Andreas
> 




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