On Thu, 15 Oct 2015, David Matthews wrote:
There's long been an issue with "use" when trying to compile and run files which themselves contain "use".
This seems as though it should achieve the desired effect with the minimum change to existing programs but there are other alternatives. For example, should it look first relative to the parent directory?
Isabelle used to use the built-in scheme for "use" of the underlying ML system in distant past. There were many special cases and sources of confusion. Over the years we have reworked that many times.
Today we have rather simple and rigid scheme:
* Each source file has a "master directory" (what you have called "parent directory" on this thread).
* Loaded resources always/unconditionally prepend the master directory of the enclosing file, without checking presence in the file system.
This means there are no "disjunctions" in how resources of a project are resolved.
Moreover there is no dependence on the file-system state. The latter aspect is particularly important in the IDE: it allows to manage resources abstractly without the physical file-system. The IDE could also create required but missing resources on the spot.
Makarius