Re: [isabelle] 2014-RC1 issues



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.


	Makarius




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