[isabelle-dev] Extracting dependencies from theory headers

[Makarius]

On Thu, 30 Dec 2010, John Matthews wrote:

> Another question: If the user asks Isabelle to process theory A, and 
> theory A has statement
>
> imports "dir1/B"
>
> and theory B has statement
>
> imports "dir2/C"
>
> then will Isabelle look for theory C in dir1 or dir1/dir2 ?
>
> In other words, does master_dir change to the enclosing directory of the 
> theory being imported?

Yes, the master directory changes accordingly.  This is what I meant with 
the sentence below:

> On Dec 30, 2010, at 5:17 AM, Makarius wrote:
>> the master directory, which is the location of the enclosing theory 
>> file when traversing the import graph.


Here is also the ML version of it: 
http://isabelle.in.tum.de/repos/isabelle/file/00b2b6716ed8/src/Pure/Thy/thy_info.ML#l276

The idea is that resources are references relatively to each theory node, 
without any further complications getting in between.


 	Makarius