On Tue, 20 Oct 2015, Tjark Weber wrote:
What may be missing in SML is a way to determine the name and path of the file that is being 'used.'
In Isabelle/ML (which is not SML) this can be done like this:
Position.file_of @{here}
where @{here} identifies its own position in the ML source via the abstract type Position.T; the fileprojected from it is (string option) since ML source does not necessarily reside in a file.
There is another subtle semantic problem, because the file-name is usually physical, and thus subject to the accidental situation at compile-time. Moving the compiled application later will render this invalid.
In Isabelle the latter happens when "the world" (e.g. the HOL image) is compiled and later moved around. There is a special trick to fold the compile-time ISABELLE_HOME directory prefix into the symbolic variable $ISABELLE_HOME, so it can be derefenced dynamically at run-time.
Makarius