10.2 Downloading

LIBRARY         ::=   ... | library URL? LIBRARY-ITEM*
LIBRARY-ITEM    ::=   ... | DOWNLOAD
DOWNLOAD        ::=   download URL SPEC-NAME-MAP+
SPEC-NAME-MAP   ::=   spec-name-map SPEC-NAME? SPEC-NAME
URL             ::=   url SITE? DIRECTORY
SITE            -- structure insignificant for abstract syntax

A DOWNLOAD specifies which definitions to copy from a remote library, with possible renaming as indicated by the optional SPEC-NAME? in a
SPEC-NAME-MAP. Any unmentioned remote definitions to which the downloaded definitions refer are copied too, but their names are not added to the global environment. Thus a DOWNLOAD shows exactly which specification names are added to the initial global environment of the LIBRARY in which it occurs, allowing references to named specifications in the LIBRARY to be checked before copying the definitions from the remote library.

[HB] DOWNLOADs are supposed to contribute to the initial global environment of a library but since they are ordinary LIBRARY-ITEMs, they may occur anywhere in the definition of a library, not just at the beginning. Does this not contradict linear visibility?

Discharged: Within libraries we still have linear visibility, so they contribute to everything that follows.

Cyclic or self-referential downloads are not allowed.

URL             ::=   url SITE? DIRECTORY
SITE            -- structure insignificant for abstract syntax

The DIRECTORY of a URL identifies the location of the library definitions at the specified SITE. When the SITE is omitted, the DIRECTORY is interpreted relative to the URL specified in the enclosing LIBRARY.

[TM] What happens if there is no URL in the enclosing LIBRARY?

Discharged: Reword: the DIRECTORY is interpreted locally with respect to the enclosing library.

---

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk