On 30.12.2010 14:17, Makarius wrote:
Last summer I've made another round in clearing out the confusion, working towards a stateless model based solely on the master directory, which is the location of the enclosing theory file when traversing the import graph. Thus the implicit use of current directory or load path can be discontinued eventually, but user theories have to be adapted a bit.
What do you intend as the replacement of the load path? For things like HOL/Library or the AFP, named roots (i.e. paths like "AFP:Abstract-Rewriting/Abstract_Rewriting") could do the trick, but I don't see what is wrong about a properly implemented load path (i.e. paths not stored in images; without the relative path naming anomalies I outlined above; maybe distinguishing between references relative to the master_dir or to the load path, like '#include "..."' and '#include <...>' in C).
Absolute paths like you introduced in 64cd30d6b0b8 only work for core Isabelle, not for the AFP.
-- Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
