Re: [isabelle] 2014-RC1 issues
- To: Lars Noschinski <noschinl at in.tum.de>
- Subject: Re: [isabelle] 2014-RC1 issues
- From: Makarius <makarius at sketis.net>
- Date: Sat, 2 Aug 2014 20:23:11 +0200 (CEST)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <53D9E56A.firstname.lastname@example.org>
- References: <1406708816.2398.53.camel@lapbroy33> <alpine.LNX.email@example.com> <53D9E56A.firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 31 Jul 2014, Lars Noschinski wrote:
Often, the "Ignoring duplicate rewrite rule/intro/..." warnings get
annoying, as they are not always meaningful (for example, overwriting
intro by intro! triggers a warning). In particular, in certain
locale-heavy theories (HOL-Algebra comes to mind), interpreting (or
opening) a locale gives you a number of these warning and there is not
always a (nice) way around them (I'd even claim that these warnings are
mostly vacuous for theory interpretations, but this is another topic).
This touches general questions about these particular historic warnings.
Many other tools have already become smarter concerning relevance of
messages. It is a long term effort to sort this out further.
The is already Context_Position.is_visible for tools to check if the
situation is right for warnings. The system does not always maintain that
properly though, and many tools ignore it.
BTW: I just discovered that symbol completion works now in the
text-boxes in the panels, very nice!
Did this behaviour change wrt. Isabelle2013-2? It should be mostly the
same as before.
This archive was generated by a fusion of
Pipermail (Mailman edition) and