Re: [isabelle] RC1 - Greyout

On Thu, 21 Jan 2016, Peter Lammich wrote:

Sorry, this was a false alarm. The thing was stuck at an error on an invalid theory path quite early in the dependencies. The error was displayed as a small red bar in the theories panel, but I simply overlooked it ...


Also note that the word "grey out" no longer makes sense in Isabelle2016, because the "greying" is restricted to the small text overview column, so "out" is not applicable: the main text view remains fully coloured.

Is there another view that is more suitable to spot errors in big projects with dozens or even hundreds of theories?

The places to look are the Theories panel and the text overview column (of individual text areas). The latter now shows everything for the document node, thus it is a small improvement.

Bigger improvements need to wait until there is a separate "Messages" panel, or similar. It was meant to come shortly after the "State" panel, but that caused so many social problems that it sucked up much more resources than anticipated.

In summary: I always need tangible and constructive problem reports; then things can be improved.


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