Re: [isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Lars Hupel
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

Re: [isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Andreas Lochbihler
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

Re: [isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Andreas Lochbihler
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

[isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Lars Hupel
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