[isabelle] file name of export_code
I have an export_code ... file "foo.ML" statement.
However, the file "foo.ML" is created in the directory of the theory
where the Isabelle-process was first started on, that is not necessarily
the directory of the theory containing the export_code statement.
This currently results in getting ML-files of different ages splattered
around my thy-directories, depending on what theory I load first.
Is there a way to place the generated code file in the directory of the
theory that contains the export_code statement?
There seem to be some shortcuts like "~~" for the isabelle-home
directory (?). Are those shortcuts documented somewhere? Is there
perhaps even a shortcut for the directory of the current theory file?
Regards and many thanks in advance for any hints,
This archive was generated by a fusion of
Pipermail (Mailman edition) and