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?

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-September/msg00056.html

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 arbitrary nesting.


	Makarius





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