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

The reason is that antiquotations are processed separately. I'm not sure
if there is a better solution, but I always "disable" them individually
by removing the @ or putting a space after it. That does it. Not very


Rafal Kolanski schrieb:
> 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.