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 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. Sounds entirely reasonable to me. > 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. Is anyone in particular working on that? Cheers, Gerwin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
