[isabelle-dev] Proposal for localized interpretations

[Jasmin Christian Blanchette]

Hi Makarius,

>> I would expect that if Jasmin's plugin manager is also used in the code generator, it would be easy to implement plugin selection for code_datatype, too.
> 
> This should work out easily with the unified Plugin_Name and Plugin concept of http://isabelle.in.tum.de/repos/isabelle/file/1891f17c6124/src/Pure/Tools/plugin.ML
> 
> Plugin_Name.declare and related operations manage a name space of plugins for commands, with semantic completion etc.  The operations around Plugin_Name.filter allow a command to restrict the use of plugins systematically.
> 
> (A potential source of user confusion is the unchecked combination of all plugins with all commands in the name space, i.e. the semantic completion may offer a plugin for a command that is not known to it.  On the other hand, commands may be built on top of each other, and I did not want to add further complexity for some inheritance system of plugins.)

It's quite nice as it is. Thanks!

Andreas: I think I promised to help you with the code generator and "code_datatype" (cf. our private email conversation about "Quickcheck & Codatatypes"). I don't understand "code_datatype" (or what you do with it) well enough to do it without guidance, but if you are still interested please relaunch me on that, ideally after December 7.

Jasmin