Re: [isabelle] signature of ml_antiquotation.ML: inline, value, embedded, etc.

Hi Makarius,

Thanks for the hints. I am very well aware of what you call an
"induction over the sources" and do it all the time. In this particular
case, however, I got lost because there are no extra headlines and
chasing down the definitions for the flag "embedded" left me puzzled (I
stopped at `update_reports` in `antiquote.ML`). I'd find a note about
the meaning of the flag `embedded` helpful.

Thanks and best wishes,


On 12.10.21 17:48, Makarius wrote:
> On 11/10/2021 12:13, Kevin Kappelmann wrote:
>> I fail to understand the signature provided by
>> `Pure/ML/ml_antiquotation.ML` (see below).
>> Can someone explain the meaning of `declaration`, `inline`, `value`, and
>> `special_form`? Moreover, what is the meaning of `embedded` (e.g.
>> `inline` vs `inline_embedded`)?
> Isabelle sources are written for the human reader, but one needs to read them
> properly:
>   0. Overview: read the signatures as entries in "table of contents" of a
> module (not as "specifications").
>   1. Look inside: the definitions in the body tell how things are constructed
> from more basic things. Usually there are extra headlines and other clues in
> the source text.
>   2. Look outside: do a hypersearch in Isabelle/jEdit as "induction over the
> sources" to see how certain items are being used. This implicitly defines
> intended semantics for them, and provides examples.
>> val special_form: binding -> string -> theory -> theory
> I don't see this in the published Isabelle2021, which is the implicit context
> of this mailing list. If you have a different version, you need to say which one.
> The terminology "special form" is standard in LISP.
> The terminology "embedded" refers to Isabelle embedded languages, normally via
> cartouches. The idea is also from LISP, but the syntax from myself after
> staying > 3 years in France.
> 	Makarius

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