[isabelle-dev] Proposal for localized interpretations

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Nov 21 14:09:40 CET 2014


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



More information about the isabelle-dev mailing list