[isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator

[Fabian Immler]

Am 07.05.2013 um 09:59 schrieb Fabian Immler <immler at in.tum.de>:
> For conceptual advances, there has also been the idea of providing a slot for "pragmas" for serializers:
> One use-case is the need to add pragmas for the target language in the generated code, but they could also be used to advise a serializer to export only specific constants -- and these pragmas could be generated e.g. by the export_code statement.

Another use case for pragmas would be the option to add (or modify) the (at the moment) hard-coded import statements, as proposed in [1].

Best,
Fabian

[1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/6887