On Wed, 22 Dec 2010, Gerwin Klein wrote:
I would think that only one search path is necessary, but I don't
understand what is meant by master_dir, I missed that part of the
discussion.
This thread is getting almost as entangled as the history of the sources
for this long standing issue.
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.
In Isabelle/00b2b6716ed8 the legacy status of the load path feature is
made explicit. I have also cleared out the Isabelle distribution already.
AFP/00b2b6716ed8 still has approximately 200 files that are located via
the "secondary search path", as can be seen by grepping for that text the
log files.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
