[isabelle-dev] Extracting dependencies from theory headers

[Lars Noschinski]

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