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
elegant.

Tobias

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.