This issue compiles a list of nice-to-have things in the MkDocs site:

• A "prettier" button for toggling the hidden source code
• Consistent font size for code blocks (the size currently in use is too big in comparison with the font size of the text)
• More readable Agda colorscheme when using dark mode
• Link from each page to the file in the GH repo (in addition or replacing the GH link on top)
• Automatically unhide code when jumping to it from the search bar
• Restrict the search bar functionality to md files (or text e.g.,)
• Rendering of meta information (typechecking times, GH activity ...)
• Table of contents for individual pages on the rhs
• "Show more Agda" button should probably only show up on pages where there is more code to show---i.e., where there are hidden code blocks.
• Add hover-over tool tips for Agda tokens.
• Improve TOC on lhs of site.