*** General *** * Commands 'generate_file', 'export_generated_files', and 'compile_generated_files' support a stateless (PIDE-conformant) model for generated sources and compiled binaries of other languages. The compilation processed is managed in Isabelle/ML, and results exported to the session database for further use (e.g. with "isabelle export" or "isabelle build -e").
This refers to Isabelle/0403b5127da1, which also contains the documentation in the isar-ref manual as usual. Examples are in AFP/390cb3cbebad: theories Diophantine_Eqns_Lin_Hom.Solver_Code and Buchi_Complementation.Complementation_Build as before, but now using the Isar command 'compile_generated_files'. This provides a better overview of incoming and outgoing files in concrete syntax, including hyperlinks to various physical and logical locations. From my side that finishes the functionalities for stateless generated / exported files for the Isabelle2019. If anything is still missing or not properly working, we have still a few weeks to sort it out. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev