[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

[Florian Haftmann]

> 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.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110825/ee327aca/attachment.sig>