Re: [isabelle] Splicing runtime ML values into Isar



Dear Lars and Makarius,

Thanks for the quick replies.

This looks like an interesting experiment. Do you think that something
similar could be done for formal comments inside types and terms, i.e.,
to change from the term language to the language context "document", as
discussed in a thread from last year?

Certainly. I only discovered that terms may contain cartouches by
accident, but given that, the possibilities for embedded syntax are endless:

   syntax "_doc" :: "cartouche_position â 'a â 'a" ("DOC _ (_)")

This allows you to write

   term "(DOC âabcâ 3) + 4"

Of course, a suitable parse translation is required to make some sense
of "abc".
The parse translation is the problem, as Makarius has pointed out. At the moment, I use informal comments (* abc *) inside terms - they are neither checked nor printed. If I knew how to formally check these comments in a parse translation, this would already be one step further, as I could then use document antiquotation to check terms, types and constants automatically. Document preparation should still work, although it would be fine for me in the first iteration to ignore these comments (as (* *) are at the moment). Is something like this possible in the current situation?

Best,
Andreas




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