Skip to content

Conversation

@NicolasRouquette
Copy link
Contributor

Add an optional declarationDecorator parameter to htmlOutputResults and htmlOutput that allows external tools to inject custom HTML into each declaration's rendering.

This follows the same pattern as the existing sourceLinker customization, enabling tools like doc-verification-bridge to add verification badges, coverage links, or other decorations to declarations without modifying doc-gen4 internals.

The decorator function receives (moduleName, declarationName, declarationKind) and returns an Array Html that is rendered after the source link.

Closes #343

Add an optional declarationDecorator parameter to htmlOutputResults and
htmlOutput that allows external tools to inject custom HTML into each
declaration's rendering.

This follows the same pattern as the existing sourceLinker customization,
enabling tools like doc-verification-bridge to add verification badges,
coverage links, or other decorations to declarations without modifying
doc-gen4 internals.

The decorator function receives (moduleName, declarationName, declarationKind)
and returns an Array Html that is rendered after the source link.
@hargoniX hargoniX merged commit 5b5f81c into leanprover:main Jan 16, 2026
1 check passed
@NicolasRouquette NicolasRouquette deleted the feat/declaration-decorator branch January 16, 2026 15:37
@NicolasRouquette
Copy link
Contributor Author

Thanks!

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.

Feature Request: Declaration Decorator Hook for External Tools

2 participants