[isabelle-dev] export_code theory wildcard exports too much

[René Neumann]

Hi,

I'm currently trying to "mitigate" the changes to export_code, which
only inserts needed constants into the signature. For one theory, I
tried to use the wildcard "Theory._" -- but the then-generated code
seems to include ALL exportable definitions of some point in time. For
example, the generated code now includes the structures
Quickcheck_Exhausting and Quickcheck_Narrowing, which seems rather odd.

The documentation states "referring to all executable constants within a
certain theory by giving name._", and I thought 'within' herer refers to
'defined in', opposed to 'available in'.

> hg id
8fcbfce2a2a9 tip

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4946 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140613/7d27c202/attachment.p7s>