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

[ mkdoc ] Wrap declaration part in <code> tag #2121

Merged

gallais merged 1 commit into idris-lang:main from gemmaro:mkdoc-code-tag

Nov 18, 2021

Contributor

gemmaro commented Nov 14, 2021

In this pull request, the declaration code in the HTML document generated by --mkdoc option will be changed to be enclosed in <code>.

This should improve the semantic meaning of the generated HTML markup.

The "declaration part" here means the area shown in the screenshot below:

See also

A very similar past example was found in Rustdoc.
- Issue: rustdoc, when I use google translate, that translate the doc as well as the code.
- Pull request: [rustdoc] Wrap code blocks in <code> tag


          [ mkdoc ] Wrap declaration part in <code> tag

mattpolzin added documentation enhancement labels

Member

gallais commented Nov 17, 2021 •

edited

Loading

I wonder whether this should be done with a new Code annotation in Idris.Doc.String or is it
the case that Decl always wraps (and is the only thing wrapping) code?

Edit: I suppose that, in the meantime, we can merge this PR. Perfect being the enemy of good & so on.

gallais merged commit c7df419 into idris-lang:main

gemmaro deleted the mkdoc-code-tag branch

November 18, 2021 22:29

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

Labels

documentation enhancement