[isabelle-dev] Towards localized syntax: bundle mixins for locale and class specifications

[Florian Haftmann]

Dear all,

my recent re-working of parts of the local theory infrastructure has
inspired me to close a long-standing gap in our module system: the
ability to organize syntax declarations into bundles and use them in
confined nested blocks

  context
    includes bundles
  begin

  …

  end

so far did not extend to class and locale specifications, which by their
very nature are always given at the outermost specification layer.

Taking the existing »includes« syntax as a base, the result looks as
follows:

  locale / class foo = import +
    includes bundles
    fixes …
    assumes …
  begin

  …

  end

The declarations from the given bundle(s) are active for the locale /
class specification itself and the optional following context block.

For consistency, also the syntax for re-opening of named contexts is
extended:

  context foo
    includes bundles
  begin

  …

  end

This is effectively equal to

  context foo
  begin

  context
    includes bundles
  begin

  …

  end

  end

See src/HOL/ex/Specifications_with_bundle_mixins.thy for examples.

This refers to rev. 589645894305.

NEWS entries and documentation updates have still to be written, but I
want to discuss possible alternative syntactic notations in a separate
thread.

Cheers,
    Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201101/20510757/attachment.sig>