[isabelle] file name of export_code

Hi all,

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 MHonArc.