[isabelle-dev] Extracting dependencies from theory headers

[Alexander Krauss]

>> Last summer I've made another round in clearing out the confusion,
>> working towards a stateless model based solely on the master directory,

> 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

The main point now is to remove old features rather than add new ones.

> Absolute paths like you introduced in 64cd30d6b0b8 only work for core 
> Isabelle, not for the AFP.

Note that paths may contain environment variables from the settings. So 
for now we could use the convention that $AFP is the thys directory of 
the afp. This pretty much does what you propose. The IsaFoR project uses 
this approach already.

Alex