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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
