[isabelle-dev] Proposal for localized interpretations

[Florian Haftmann]

Hi Andreas, hi Jasmin,

> 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.

In my understanding, this seems quite trivial.  The first step is to
formally generalize the existing registration functions with
Plugin_Name.filter arguments (from data_default to data):

http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/Pure/Isar/code.ML#l1253

http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/Pure/Isar/code.ML#l1275

Then the input syntax is adjusted accordingly using
Pluing_Name.parse_filter, e.g.

http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML#l1081

Does this help?

All the best,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141126/3281df33/attachment.sig>