[isabelle-dev] Confusion aroung master path of theory
florian.haftmann at informatik.tu-muenchen.de
Fri Jul 20 17:56:56 CEST 2012
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. 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?
b) If the »master directory« is not the concept to achieve this, what is
it then supposed to be?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev