On Fri, 20 Jul 2012, Florian Haftmann wrote:
cs. http://isabelle.in.tum.de/repos/isabelle/rev/3a5a5a992519 was an
attempt to make results of `export_code` with relative file path more
predictable. There my assumption was that Thy_Load.master_directory
would point to an absolute path, particulary the location of the current
theory, but this was a guess. Now I see that in most cases it just
points to `.`, which contradicts my previous understanding that the
master directory concept would make the notion of current working
directory obsolete.
This depends on some side-conditions. I guess that you have run "isabelle
tty" or "isabelle-process" here. This implicitly requires to cd to the
session directory, just as usedir does before running the tty process.
The Isabelle/Scala document model is in a transitory state where the
master_directory works in fully stateless manner in most situations. So
in Isabelle/jEdit Thy_Load.master_directory should work.
Proof General has its own traditional way to "cd" along with the files
being processed, which it has been upgraded at some point to use the
master directory as well, so it should also work.
http://isabelle.in.tum.de/repos/isabelle/annotate/3ceccd415145/src/Pure/ProofGeneral/proof_general_emacs.ML#l254
So, to lift my confusion, two questions:
a) Is there a way to interpret a given relative path as relative to the
(absolute) location of the current theory?
File.pwd () gives you an absolute path, and you can just use Path.append
as usual. Note that the Path algebra does the right thing when two
absolute paths are appended: the first one is ignored.
b) If the »master directory« is not the concept to achieve this, what is
it then supposed to be?
The master directory is basically correct, modulo some fine points.
One potential snag is that the master directory might not be writable at
all, because it is some URL obtained via the IDE front-end, or since the
prover is not on the same file-system as the front-end. This touches an
open question that is beyond the small issues at the moment, and it is not
fully active right now.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
