On 11/01/2019 11:51, Makarius wrote: > On 10/01/2019 16:38, Makarius wrote: >> On 10/01/2019 16:28, Florian Haftmann wrote: >>> Code generation: command 'export_code' without file keyword exports >>> code as regular theory export, which can be materialized using tool >>> 'isabelle export'; to get generated code dumped into output, use >>> 'file ""'. Minor INCOMPATIBILITY. >>> >>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc >>> generated code in AFP-entries. >> >> Great, I will try this out soon. > > I have started looking and thinking about it again.
I have reworked this a bit in Isabelle/e61b0b819d28: Isabelle/jEdit is able to browse theory exports via the virtual file-system "isabelle-export:" and the 'export_code' command emits some information message about it. There are still a few open questions: * Are there remaining uses of 'file' with empty name? Is the virtual file-system browser sufficiently convenient to inspect results interactively? * How to specify proper (unique) export names: PIDE still lacks a check for uniqueness of export names, but overwriting existing exports is considered illegal. The 'file' allowed to produce separate names in the past, but it has a different meaning now (and is a candidate for deletion). Maybe 'export_code' should be renovated replaced by reformed commands like this: * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is optional and the default something like "generated" or "code". This could be a "thy_decl" command that updates the theory context by generated files that are accessible in Isabelle/ML, in addition to the export; it would also include a check for duplicate names. * "code_checking CONSTS in LANGUAGE" -- observing that "export_code ... checking" is actually a different command. It would be a "diag" command as before (this is relevant for parallelism). Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev