Skip to content

Conversation

@johnbartholomew
Copy link
Collaborator

Uses AnchorJS: https://www.bryanbraun.com/anchorjs/

It could be done without JS, which might be nicer, but the docs already use JS (and WASM) to serve the codemirror, interactive elements, and also the MathJax formatting for the detailed language specification. For now, using AnchorJS provides an easy fix. Note that the actual heading elements mostly (all? I haven't checked every individual one) already had id attributes which can be referenced in the URL fragment; they just didn't have a visible link for someone to copy.

Fixes #1104.

https://www.bryanbraun.com/anchorjs/

AnchorJS is under the MIT license.
This bundle is direct from:
https://github.com/bryanbraun/anchorjs/blob/14e912226316aea775d957fa96c295193157f31d/anchor.min.js

Doesn't seem much point in messing with NPM for this, it is a small and
fairly simple script.

(I unminfied and checked for signs of malicious content, it seems fine)
The standard library gets some extra attention here, to put anchor links
onto each of the entries individually.
Since we're now providing visible anchor links, it's important that
ID attributes on headings are genuinely unique.
@johnbartholomew johnbartholomew merged commit 79820ad into google:master Feb 25, 2025
6 checks passed
@johnbartholomew johnbartholomew deleted the doc-anchors branch February 25, 2025 00:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Jsonnet.org - make headers links

1 participant