Dear users of the code generator,
last week I spoke with Florian about some fundamental properties of the
code generator.
Many Isabelle users are also "power users" of the code generator; in the
sense that they exploit many of its facilities (code printing, various
attributes, ...). These days th
Dear Lars,
On 24/07/17 15:08, Lars Hupel wrote:
1) Function transformers: I want to run a function transformer in
special situations. But I can only register it globally (with
"Code_Preproc.add_functrans"). What I use is the following pattern:
val enabled = Attrib.setup_config_bool @{binding "c
Dear Andreas,
> Well, we here at ETH have another function transformer, which can also
> be activated and deactivated basically with almost the same pattern. The
> only difference is that at the moment we use a command rather than a
> Config value because de- and reactivation in our case has to do
Dear Lars,
Well, we here at ETH have another function transformer, which can also
be activated and deactivated basically with almost the same pattern. The
only difference is that at the moment we use a command rather than a
Config value because de- and reactivation in our case has to do a bit
mo