[isabelle-dev] Extracting dependencies from theory headers

[Makarius]

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