Re: [isabelle] RC1 - Greyout
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] RC1 - Greyout
- From: Makarius <makarius at sketis.net>
- Date: Thu, 21 Jan 2016 16:47:18 +0100 (CET)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <Z005fbs0LF6xvh2.RZmta@smtpin.rzone.de>
- References: <Z005fbs0LF6xvh2.RZmta@smtpin.rzone.de>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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