[isabelle-dev] Extracting dependencies from theory headers
makarius at sketis.net
Thu Dec 30 21:21:11 CET 2010
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:
The idea is that resources are references relatively to each theory node,
without any further complications getting in between.
More information about the isabelle-dev