Re: [isabelle] Isabelle2013-1-RC1 available for testing

On Mon, 7 Oct 2013, C. Diekmann wrote:

When using code_modulename, the buffer displays a Warning:
"Legacy feature! prefer "code_identifier" over "code_modulename""
However, the warning is not visualized by jEdit (I expected a yellow
marking at the left border)

Florian Haftman is emitting a warning in the parser of the command, so it ends up in slightly different slots than messages produced at actual run-time. Since some related legacy warnings already happen at runtime, I have now adapted code_modulename accordingly -- for the next release candidate that is anticipated during this week.

Warning, tracing, error messages are notoriously difficult to get right in all respects, since they only happen in special situations. Legacy message are particularly bad, since they are to disappear anyway together with the old feature that they inform about. This is called in Isabelle jargon "renovation before demolition".


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.