[isabelle-dev] Explicit option "open" for code_reflect

[Florian Haftmann]

Hi Fréderic,

> Between Isabelle 2014 and 2015, the option "open" appeared for the
> command export_code, and by default the reflection minimizes the
> exported code.
> Would it be acceptable for code_reflect to also have a similar option
> "open"?

what is your use case?  If you want to export an operation in the
generated code, just add it to the list of constants.  It is the very
purpose of code_reflect to provide a well-defined interface.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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