[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 21:41:26 CEST 2011
> When I've seen the "complete_boolean_algebra" incident on the other
> thread my first impulse was to check how far the wiring of the class
> package wrt. the Isabelle document markup was. In principle the prover
> can provide useful clues in non-intrusive ways here, if done right.
> E.g. in Isabelle/jEdit one can hover over the text with COMMAND/CONTROL
> to ask "What is this?" and often get useful feedback already.
> Unfortunately, the class package is still in a confusing state here, so
> I did not even put it on the list of things to be done, because it is
> just another instance of similar ongoing reforms, and there are so many
> really pressing things in the pipeline. (Quite a bit has happened here
> already, like purging the name space module from historic cruft one more
> time, and assembling all syntax layers clearly in one place.)
I dimly remember that one day I had planned to return to the class
package (awaiting a trigger which in fact has not fired until now).
I guess the problem is somehow about dealing with bindings the right way
to preserve markup which has to be added, but I am far from
understanding what actually has to be amended. Maybe at a certain time
you can give me further hints.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev