Skip to content

Features

The following features of the MaterialX theme can be used in websites generated by Agda Pages (the names below are linked to the the feature documentation):

The Agda-Pages Demo website is built with the default features defined in agda-pages-features.yml. This includes all the features listed above except navigation.expand, navigation.footer, navigation.prune, navigation.sections, and toc.integrate.

To use a custom feature list for your generated website, override the value of theme: features inherited from Agda-Pages: add a copy of the agda-pages-features.yml to your properdocs.yml, then edit your copy. See also the MaterialX configuration template.

Note

ProperDocs does not support multiple uses of INHERIT in properdocs.yml. However, an inherited file can itself inherit from another file.

Larger websites

The default theme features do not include the navigation.expand feature. This feature is likely to result in an inferior user experience (UX) for larger websites where top-level sections have more than about 50 pages, because the navigation panel may then require scrolling to access some subsections.

Also the navigation.footer feature is undesirable on larger websites with generated pages that list Agda modules: the links to the previous and next pages are based on the module names in lexicographic order, which might not be an appropriate browsing order.

Another point to bear in mind is that by default, all pages of a generated website include the HTML for the complete navigation hierarchy of the current section. For websites with hundreds of pages, that can make page loading quite slow. Adding the navigation.prune feature replaces each expandable section in the navigation panel with a link to the first page in that section – thereby significantly reducing the size of the pages. The drawback is that users can never browse the full navigation hierarchy, but this is mitigated by the hyperlinks from names to declarations in the Agda code listings. Whether to add navigation.prune depends on the significance of page and website size for your expected users.

Agda code is usually organized as a hierarchical collection of modules. Modules can be nested, named, and defined in separate files. Agda requires the name of a top-level module to match the name of the file and directory in which it is defined: a top-level module named A.B.C has to be the (first) module defined in the (plain or literate) Agda file C in the directory A/B.

Agda Pages generates webpages from top-level modules. The files and directories correspond closely to those in which the modules are defined: usually, Agda Pages generates the Markdown source code for the webpage listing module A.B.C in the file docs/A/B/C.md. The module navigation panel of the generated website can then display C as a link to that webpage in the subsection B of section A.

Refactoring a module A.B.C to import a collection of modules A.B.C.D, A.B.C.E, etc., defined in separate files, requires adding the directory A/B/C. By default, the navigation panel now displays C as a link to the webpage listing A.B.C, as well as as an expander which (when clicked) reveals links D, E, etc., to the webpages listing the corresponding modules.

The default theme features include navigation.indexes. When there is a section index page docs/A/B/C/index.md, this feature links the directory name C in the navigation panel directly to that page. Also by default, the make-command to generate webpages detects that the module A.B.C is defined in a file that has the same name as a sibling directory, and moves docs/A/B/C.md to the location docs/A/B/C/index.md.

Warning

The module hierarchy should not include both A.B.C and A.B.C.index, because the generated pages would compete for the same URL: A/B/C/.

Thus by default, the navigation panel displays C only once. Clicking on it not only expands to reveal the links D, E, etc., it also opens the webpage listing A.B.C or A.B.C.index. This seems optimal when that module merely imports modules A.B.C.D, A.B.C.E, etc.

However, the default treatment has a potential drawback: users could easily overlook a module A.B.C (or A.B.C.index) which gives an informative overview of a collection of imported modules. For a website listing a hierarchy of Agda modules where each section index page provides such an overview, it seems best to remove the navigation.indexes feature.