[isabelle-dev] Confusion aroung master path of theory

[Florian Haftmann]

Hi all,

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?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120720/080971bd/attachment.asc>