[isabelle] Isabelle annotations being processed in comments in ML files?



Dear Isabelle Users,

I have found that when including an ML file with:
	"use blah.sml"
if I have an annotation like @{const_name "doesnt_exist"} in a statement, then commenting it out doesn't stop the "unknown constant" error when processing the ML file!

Is this behaviour intentional? Is there any way to actually comment out a block of code AND its annotations?

Yours Sincerely,

Rafal Kolanski.





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