*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Formal comments within inner syntax*From*: Makarius <makarius at sketis.net>*Date*: Wed, 10 Sep 2014 21:30:11 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <541012A9.8040008@inf.ethz.ch>*References*: <54097E7E.5000706@inf.ethz.ch> <54100BA7.2080300@informatik.tu-muenchen.de> <541012A9.8040008@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 10 Sep 2014, Andreas Lochbihler wrote:

Your suggestion looks very much like JavaDoc comments. However, I amless interested in formally checking that every parameter is documentedrather than formally checking the documentation. So your suggestedapproach provides only little over what is currently available withoutthe 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 thelanguage 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.

Makarius

**References**:**[isabelle] Formal comments within inner syntax***From:*Andreas Lochbihler

**Re: [isabelle] Formal comments within inner syntax***From:*Florian Haftmann

**Re: [isabelle] Formal comments within inner syntax***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle 2014 and proof general
- Next by Date: Re: [isabelle] Simple selective code generation?
- Previous by Thread: Re: [isabelle] Formal comments within inner syntax
- Next by Thread: [isabelle] Quickcheck in locale with defines directive
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list