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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
