Re: [isabelle] simp warnings for cong rules



On Mon, 11 May 2015, Larry Paulson wrote:

This behaviour is inherited from the way things were 20 years ago, when what is now deeply buried was itself the user-facing operation.

Indeed, that was a rather different era, in the depths of time of Isabelle history. It vaguely reminds me of the "real mode" of x86 CPUs: http://en.wikipedia.org/wiki/Real_mode

Today it is a bit challenging to emit warnings (or other markup) in a way that makes proper sense to the user. Context_Position.is_visible is already well-established as a guard for most messages. Last year I also introduced Context_Position.is_really_visible for Simplifier declarations, to reduce spurious yellow in the PIDE markup. Such things are always dangerous: there is more and more complication, and problems ultimately don't get solved.

Right now, I have no particular opinion in which direction to move. If certain warnings can be removed altogether, they cannot cause further problems.


	Makarius




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