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