[isabelle-dev] NEWS: commands for generated files

[Makarius]

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