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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
