Re: [isabelle] Formal comments within inner syntax



On Wed, 10 Sep 2014, Andreas Lochbihler wrote:

Your suggestion looks very much like JavaDoc comments. However, I am less interested in formally checking that every parameter is documented rather than formally checking the documentation. So your suggested approach provides only little over what is currently available without the antiquotations
@{spec} and @{arg}. In particular, the problem of
linking the parameter positions and types remains.

Do you have any idea how one could escape from inner syntax to the language context "document"?

On 10/09/14 10:28, Florian Haftmann wrote:

 a radical answer would be to allow inner syntax to contain arbitrary
 text cartouches ‹…› but I guess this would be a too massive change.

Inner syntax already allows cartouches, e.g. see the isar-ref manual about outer and inner syntax, or more practically $ISABELLE_HOME/src/HOL/ex/Cartouche_Examples.thy (which is just a playground of possibilities collected in chronological order over some weeks).

It remains to be seen where cartouches make most sense in actual use in Isabelle/Pure and Isabelle/HOL. The full potential still needs to be fathomed.


For the concrete problem of inner text blocks, I reckon that it could be done, assuming that the document preparation system finally manages to warp forwards in time from 1999 to 2014. So many important reforms are still in the pipeline, such as proper support for nested markup and nested formal languages for LaTeX rendering. With that available, the "escape" from inner syntax to the document language would just be normal nesting of languages with corresponding change of rendering.

I have envisioned something like that many years ago, but it did not get through the pipeline so far, due to the tight entanglement of the document preparation system and its many sophisticated tricks. There is also a correspondence to the "too many modes" problem of checking Isabelle theories in batch build mode, versus PIDE interaction mode, versus two obsolete TTY modes.


	Makarius


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