[isabelle-dev] Code generation in Isabelle

[Makarius]

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.


 	Makarius