Re: [isabelle] Splicing runtime ML values into Isar
On Wed, 10 Jun 2015, Andreas Lochbihler wrote:
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?
You can of course embed something that looks like document source within
terms, or any other Isabelle language.
The remaining problem, though, is to have the document preparation system
present it properly: that is a bit old, it only looks at the outer syntax
for pretty printing.
To get this right, a substantial reform of the Isabelle document
preparation is required, to "print" everything formally from the depths of
This archive was generated by a fusion of
Pipermail (Mailman edition) and