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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
