Re: [isabelle-dev] Extracting dependencies from theory headers

2011-01-03 Thread 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 dir

Re: [isabelle-dev] Extracting dependencies from theory headers

2011-01-03 Thread Gerwin Klein
On 31/12/2010, at 12:17 AM, Makarius wrote: > 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 h