Re: [isabelle] Splicing runtime ML values into Isar
Dear Lars and Makarius,
Thanks for the quick replies.
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?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and