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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
