<\body> <\make-title> > The development of a robust linking system for is important for many aspects of the program: <\itemize> Usual labels, references, hyperlinks, actions. Links to automatically generated content (citations, tables of contents, indexes, ). Multi-document editing. Observers (used to observe a resource which is subject to change); may be used for automatically generated output from computer algebra or proof systems. Spreadsheeds. Document enrichment with automatically generated links (Wiki) or third party links. Document extraction based on typing information and litterate programming. Typed links for annotation, documentation traversal information, contextual browsing, Collaborative editing. Our approach is similar to in several respects, but it differs at certain points: <\itemize> Since is not attribute-based, attributes correspond to tags, which can either be used in an attribute-like fashion or in the content itself (using the concept of the current englobing locus). Local and distant resources ( and ) correspond to different types of ``loci''. In contrast to , a locus identifies both a place and the corresponding (linking) environment. In particular, linkbases can be considered as special cases of loci. An alternative implementation would be to consider linkbases as different objects and to provide markup for associating a linkbase to a locus, or to link a locus to its corresponding linkspace using a link with a special role. does not distinguish between extended links, simple links and arcs. Links are merely relations between a finite named set of loci, according to a given set of roles. In particular, the special arc properties like and are part of the role. Roles are not merely containers with a mere pointer to an informal description. Instead, a tentative is made to invent markup which describes the behaviour of a role. Additional behaviour may be defined in plug-ins. A locus is a well-identified portion of content which can participate in a link. A locus can either be <\enumerate> Part of a local document. Part of a distant document. Part of some automatically generated data. A container for linking data. Several properties are attached to the locus: a unique identifier and one or several names, one or several roles and the linking context for the locus. <\explain> >|attr_n|content> >|attr_n> >|attr_n|content> >|attr_n> <|explain> Declare a locus of one of the four above types and encapsulate the (when specified) in the locus. The attributes are instructions for attaching properties to the locus. These instructions may also be specified the content (for instance, a theorem inside a locus may add a role to the locus, as well as data with the theorem number and the page number). Notice that loci may be nested. In that case, the inner locus inherits the linking properties from the outer locus (unless otherwise specified using the role (opposite of )) and vice versa (unless otherwise specified using the role (opposite of ); in the case of data loci, is default). The following instructions specify properties for the locus. In addition, one may use the and instructions as well as the and instructions from the next sections. <\explain> <|explain> Specify a name for the locus. In the case of , the identifier must be unique in the englobing locus (which defaults to the entire document when there is no englobing locus). For the moment, we require the specification of unique identifiers for efficiency purposes. In the future, unique identifiers should be automatically generated, and the primitive will become obsolete. When used as an attribute, one may use instead of . <\explain> <|explain> Specify a role for the locus. Roles are used to associate properties to loci which may be exploited when browsing or for other purposes. Built-in roles are , , and . <\explain> <|explain> For use in loci only. The specifies a way to retrieve the resource. Hyperlinks may either be <\itemize> Identifiers for other loci. Standard hyperlinks of the form . An expression >|role_n> intended to follow any link which matches all roles to a locus with identifier . An expression >|href_n> for specifying a union of resources. An expression for resources which are the result of the evaluation of a program, a form or a query on . <\section> Links A link associates an arbitrary number of loci. It may specify one or several roles which specify the behaviour of the link (browsing behaviour, editing behaviour, typesetting behaviour, ). <\explain> >|attr_n> <|explain> Declare a link between several loci. The attributes are instructions for attaching properties to the link. The following instructions may be used to specify properties of the links: <\explain> <|explain> Specify an identifier for the link which may be used to refer to links. <\explain> <|explain> Specify a part of the link with symbolic name and which points to (recall that may be the identifier of an other locus). The parts which are required for a given link depend on the roles of the link. Standard links with role require and parts (which correspond to the values of ). When a part of a link which is required for a given role is not present, then its destination defaults to the current locus. <\explain> <|explain> Specify a role for the link. Roles are used to associate properties to links which may be exploited when browsing or for other purposes. Built-in roles are <\description> >Standard hyperlinks. >Standard links, but without any indication on how to display or traverse the link. >Link all parts in the link. >Make all valid links for a source locus valid in a destination locus. >Automatic links from parent loci to child loci. Users may provide roles like for bidirectional links or , for applications of a theorem, for replacing the source of a link by the contents of its destination, Users may define new roles for loci and links. These roles may be abstract containers with a behaviour which is defined in a plug-in. They may also specify special properties for the role or additional constraints on the role. Locus roles and link roles which are not speci <\explain> >|attr_n> <|explain> Declare a role. The attributes are instructions for attaching properties to the role. The following instructions may be used to specify properties of roles: <\explain> <|explain> Associate one or several names to the role. <\explain> <|explain> Link to a page with an informal description of this role. <\explain> <|explain> [For link roles] The linking structure of the locus with name is taken as model for the linking structure of this role. For simple link structures, the locus would typically be a small autonomous locus. For instance, if the locus defines subloci and with standard hyperlinks from to and vice versa, then |>> would define a role for bidirectional links. The subloci and of become required parts of bidirectional links. <\explain> >|cond_n> <|explain> [For link roles] Specify (disjunctive) conditions for this link to be valid. The conditions are checked one by one for the set of candidate links. As soon as one condition is met by a non-empty subset of the set of candidate links, this non-empty subset is returned. For example, assume that we have two documents which are available in several languages: , , , and . Given a link > , we have 6 matching links. The first condition may check whether the languages of the source and destination languages coincide (the languages may either be roles or data associated to loci). A second condition may check whether the destination language is English. A third condition might always evaluate to . In a similar way, one may define conditions which privilege ``close links'' to ``distant links''. The markup for specifying conditions still has to be designed. We should probably rely on plug-ins. We may also provide markup for simple tests on matching roles or loci. <\explain> <|explain> Hints for how to render the link and when the link should be traversed (see ). All loci currently known to the editor (with the associated links) are stored in a (probably hierarchically ordered) ``loci space'', which should be considered as a database. Each locus has a unique identifier in this database. The database is constructed during the typesetting phase. Each document (or view) has a unique identifier. Two ways are provided for associating unique identifiers to loci: <\itemize> The user specifies a unique id in the englobing locus (which will be prefixed by the unique id of the englobing locus so as to yield a global unique id). The id is automatically determined using a counter relative to the englobing locus. The second method may be expensive when the englobing locus is large, since it may modify the environment. In the far future, we should associate unique ids to nodes of lazy rewriters. Loci which are no longer present may still remain in the database and references to newly modified loci may be incorrect. When an entire document is being typeset, we have to do several things: <\itemize> Move all loci for the current document to a shadow space (where they are kept during the typesetting) and remove them when typesetting is done. Collect all couples (reference, value) which are encountered during the typesetting in an auxiliary document. At the end, test whether the values are still correct. If not, then it may be necessary to retypeset the document. <\description> >The unique identifier of the current locus in the database. >For the automatic generation of a identifiers for subloci. >The contents of the locus, except for subloci, which are entered directly into the database. Each of the environment variables is locally redefined for each locus/sublocus. Notice that , , and directly affect the linkspace (and not much the environment unless an identifier is automatically generated). All other linking primitives are directly entered into . They are entered into the linkspace together with the englobing locus. When saving, all loci relative to the current document are collected and saved (without uodating). When loading, they are immediately entered in the database. Notice that the global variable should also be saved. Besides loci which are specified by the user, may also automatically generate new loci (with or without data). For instance, output from computer algebra systems might be stored in auxiliary loci before inclusion (via copying or linking) into documents. Similarly, a shared context with a proof system might be stored at an auxiliary locus. For these purposes, it may be useful to associate persistent unique identifiers to processes. This makes it possible to recognize the execution of the same program at a different time or computer. In its brute form, the link space is a collection of loci with unique identifiers and such that each locus defines a set of locus properties including the links. In order to quickly resolve links, it is necessary to (incrementally) compute a contracted version of the linkspace from which it is clear which loci and links are valid at a certain locus. For this, we will use the postulate that environment importation is always transitive. More precisely, we need to maintain a table which associates to each locus its ``cyclic closure'', the set of all loci > such that depends on > and vice versa, and the induced uncyclic graph structure on this table, which we expect (hope) to be simple in practice. As a consequence, we have a fast decision procedure for knowing whether a given locus or link is visible inside a given other locus. Next, for each name, we maintain the list of loci/links/roles in which it participates and vice versa. Assume that we need the list of links for a given locus. Then we first lookup the list of names for the locus and next the list of links participating in one of the names. Next, we filter out the links so as the keep only those which are visible in the locus. Next, we lookup the roles of each remaining link, which amounts to further filtering ( ). The remaining links are ready to be used for rendering or navigation. <\remark> Notice that importation of linking context may be subject to additional restrictions: it is reasonable to require links with the role to be outbound and defined in the locus (except for publicly exported context to parent loci). This restriction may make it easier to maintain the ``cyclic reduction graph'' in an incremental way. In practice, explicit context importation should only be used at a few places ( at the document level or in a few dedicated special tags). During the incremental cyclic closure computations it is then mainly necessary to keep track of the , , and roles of loci. <\initial> <\collection>