mkdocs site nice-to-have: hover-over for Agda tokens #947

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Draft

williamdemeo wants to merge 2 commits into master from 826-niceties-hover-over

Member

williamdemeo commented Oct 10, 2025

Description

This adds hover-over for Agda tokens so the definition of a token will appear in a pop-up box when you hover the mouse pointer over that token.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff


          first pass at hover-over

027f714

williamdemeo linked an issue

that may be closed by this pull request

Niceties to have in the MkDocs site #826

Closed

11 tasks


          second pass

d5591af

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet