Re: [isabelle] RC1 - Greyout



I've noticed that, too. Occasionally, especially when loading a large number of theories inti Isabelle/JEdit (e.g. HOL) and going back and forth a bit or when letting non-terminating proof methods run for more than a few seconds, the state output that I get does not get updated anymore with no indication that it is "stale".

Another recurring problem that I noticed is that sometimes, when loading e.g. HOL, if one jumps into the middle of one of the theories to be built while the theories have not all finished building, Isabelle will start building /all/ of them from the beginning /again/.


This behaviour is somewhat sporadic and despite some effort, I have not been able to reproduce it properly, so I did not report it before. I must also admit that I noticed this behaviour with pre-RC Isabelle; I've not had enough opportunity to use Isabelle enough inbetween to see whether this occurs with the RC as well, but Lars' and Simon's mail seem to indicate that it does.


Cheers,

Manuel


On 27/01/16 11:17, Simon Wimmer wrote:
I second that. Additionally, on RC2 I (Mac OS X) occasionally see a
spinning multi-colored circle, which might stick with me for an indefinite
amount of time during which I cannot make any input. I didn't experience
this with Isabelle 2015.




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