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. On Mon..Wed this week I visited the Innsbruck Isabelle site (the city of Innsbruck is very professional in managing a lot of snow without hindering public life :-) I've had some discussions with users of Haskell code generation, e.g. AFP/HLDE. My conclusions so far: * primary (default) output should be via the new Generated_Files module in Isabelle/ML; thus applications can refer to file content via a theory context, e.g. to write it to the file-system via Generated_Files.write_files. * secondary output works via the Export interface to Isabelle/Scala; e.g. I could easily add Generated_Files.export_files for that and export_code would merely use Generated_Files.add_files (no export yet). Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev