On Thu, 22 Sep 2011, Brian Huffman wrote:
I actually like Peter's idea of a "deprecated" flag better than my
Legacy.thy idea. We might implement it by adding a new "deprecated" flag
to each entry in the "naming" type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
identically to non-deprecated names, except that looking up a deprecated
name would cause a legacy warning message to be printed. I don't think
it would be necessary to modify any other tools or packages.
Of course, we'd also need to invent some interface for marking names as
deprecated in the first place. It might also be nice to associate a text
string to each deprecated name (perhaps saying what other name/feature
to use instead) instead of just using a boolean flag.
This would be the basic plan, but it also needs to be wired up with the
Prover IDE protocol and stylesheets (which are still only half finished).
The part about the name space is relatively easy, but the "annotation"
part in the source text requires some further thoughts. Concerning the
extra text, the attitude in PIDE is to point to the original source for
additional information. There could be a semi-formal comment telling the
user, maybe as simple as the existing "-- cmt" form. (Some people in
Edinburgh have proposed "social tagging" :-)
Anyway, I am the one who is responsible for these parts of the system. It
is old wisdom in Isabelle develoment (with its 25 years) that it is more
efficient to consult the experts and main responsable persons for each
particular component, instead of tinkering oneself. (The latter has
occasionally happened, either leading to code in terminal condition that
nobody undertstands anymore, or forcing some poor fellow to re-engineer it
from the ground up. For the name space module both has happened in
variations several times already.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
