[isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension

[Makarius]

On Wed, 4 Apr 2012, Tobias Nipkow wrote:

> Am 04/04/2012 11:48, schrieb Tjark Weber:
>> Adhering to the principle of least astonishment, I suspect an error 
>> message (or at least a warning) would be more helpful.
>
> Isabelle's well-tried principle of least astonishment is not to give too 
> many helpful error messages or warnings ;-)
>
> Actually, in this case it is not so easy to produce an error message 
> because the patterns are translated away with translations and the 
> resulting lambda's are perfectly legal.

Yes, things like %x x x x. x and fix x fix x fix x have "x = x" are 
perfectly legal and behave quite uniformly for many years, i.e. with 
little surprise to people who have got acquainted with Isabelle scoping 
rules.

To make things even more simple for beginners, the Prover IDE markup 
protocol already indicates the internal scopes in the source text.  E.g. 
when using CONTROL/COMMAND with mouse clicks, one can explore the internal 
bindings.  It is only a small addition to the display engine to make 
variable scopes immediately visible in the source text, like Netbeans 
would do for Java for example when the user moves or hovers over the text.

In contrast, lots of warning messages are old-school TTY technology, and 
in Proof General the channel for that gets easily overloaded so that the 
user is switching into SPAM mode.


 	Makarius