Re: [isabelle] file name of export_code
On Thu, 1 Oct 2009, Peter Lammich wrote:
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.
You are right, when Proof General starts the process, it uses the cwd of
the associated buffer that happens to be in front at that time. So the
result is indeed erratic.
There seem to be some shortcuts like "~~" for the isabelle-home
directory (?). Are those shortcuts documented somewhere?
It might be buried in one of our many manuals from different periods, or
Isabelle path specifications are as follows:
- Basic posix notation with ".", "..", "/" and root "/"
- environment variables $HOME, $ISABELLE_HOME, $WHATEVER, ...
- abbreviated variables: ~ for $HOME, and ~~ for $ISABELLE_HOME
The basic idea of the Isabelle environment is explained in the "system"
manual, and is in fact quite central to the Isabelle system since 1998.
Is there perhaps even a shortcut for the directory of the current theory
I've occasionally thought about things like that. Of course the
environment cannot be changed during the load process, because this would
be a global side-effect.
Maybe the notion of "project directory" would work better, i.e. an
environment "constant" that points to the root directory of a session
(where ROOT.ML is at the moment).
This archive was generated by a fusion of
Pipermail (Mailman edition) and