On 02/02/2019 14:13, Florian Haftmann wrote: > * The module naming schema gets more sophisticated: default, name or > prefix. The key point is that this naming schema is again > target-language specific.
Just abstractly, a reform should strive for unification and simplification whenever possible. The different languages have slightly different side-conditions, but maybe they can still be unified: e.g. the main NAME could become NAME.EXT or NAME/ depending on the situation. One could also use the const names to produce a default, e.g. according to the traditional scheme to concatenate const base names with "_" as separator. > This should cover all application cases. When export_code emits Generated_Files.add_files, there is always a possibility to do special-purpose Isabelle/ML programming with Generated_Files.get_files. No need to have all odd cases in one Isar command. > At the moment I am still in favour of a diagnostic command to emit sth > ad-hoc into the file system -- but this could be something separate from > export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination. For diagnostics I have used the "isabelle-export:" VFS in Isabelle/jEdit so far: if a physical file is required, it can be written from the editor (which actually cased the crash before Isabelle/9fd395ff57bc). Minor disadvantage: writing directory content is inconvenient. In that case there is also Generated_Files.write_files. Some months ago I've seen odd crashes with files written to $ISABELLE_TMP_PREFIX/ in Isabelle/ML and read in Isabelle/Scala. Moreover I've seen crashes of the Headless PIDE session of export_code with $ISABELLE_TMP_PREFIX in particular. There might be something wrong in my areas of responsibility, or something inherently fragile in concurrent access to a Unix file-system. These incidents motivated to revive the pending thread to eliminate physical files from export_code in the first place. Mathematical files in the theory context are more reliably than physical ones on a magnetic drum. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev