On 07/25/2011 10:25 AM, Makarius wrote:
On Sun, 24 Jul 2011, Alexander Krauss wrote:
Anyway, the standard procedure for removal of old stuff is to start
marking it as "old" or "legacy" in the NEWS, and emitting suitable
legacy_warnings.
I will follow that standard procedure, once all occurrences of the old
code generator invocations are replaced.
Put in legacy warnings already now, as they will alert users who
accidentially type the wrong commands (remember our experience with
the methods "evaluation" vs. "eval" last week). You don't have to
wait with this until all else is resolved.
Yes, waiting until certain things are done tends to pile up a lot of
unfinished things. The system is grown (and reduced) from the bottom
up, one well-defined step after another.
The situation "all else is resolved" is only ever achieved
asymptotically.
Legacy warnings are in place; After the next release, the SML code
generator will disappear from the HOL image.
Lukas
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
