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



On Thu, 12 Feb 2009, Rafal Kolanski wrote:

> I have found that when including an ML file with:
> 	"use blah.sml"

BTW, Isabelle/ML files should always be .ML -- not .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?

The behaviour is just a consequence of how ML antiquotations are done (not 
"annotations"): as a preprecessing step before actual ML processing. In 
particular, the antiquotation layer does not understand ML syntax, so 
there is now chance to treat them differently inside ML comments.


At a later stage, antiquotations might be more tightly integrated with the 
ML syntax.  The motivation is more substantial though: allowing to write 
ML patterns and expressions containing variables, e.g something like f 
@{term "x + y"}

As a consequence of that future refinement, comments might be treated 
differently as well.


	Makarius





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