On 31/01/2019 18:27, Peter Lammich wrote: > On Do, 2019-01-31 at 16:03 +0100, Makarius wrote: >> I have looked around at typical uses of 'export_code' in AFP. Most of >> the time it is just informative: writing a file and looking at it in >> the >> editor (or via the command-line!?), or doing that on the output >> channel. >> The isabelle-export: file-system covers that already, i.e. we should >> be >> able to eliminate almost all generated files from the AFP repository. >> >> So "export_code .. file" should just disappear -- it is semantically >> illtyped in PIDE: editing the "file" argument will leave a trace of >> machine oil spilled to the physical file-system. > > The problem here is actually deeper: > Many AFP-entries are designed to export code which then works together > with some external code. However, there seems to be no way to test > whether this external code works with the generated code.
Can you point to these special applications? If export_code uses Generated_Files.add_files (in addition to Export.export) we get both a check for unique names and an easy way to retrieve the exports in Isabelle/ML, e.g. to write to a temporary directory and do some tests. So far I have never seen an application that could not be made stateless and thus fit properly into the PIDE model. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev