Yannick Zakowski (Sep 28 2020 at 17:25): Yannick Zakowski (Sep 28 2020 at 17:25):It is cosmetic, but I am hating the following behavior with a passion. In the refman, say I search for selector because I want to check something about goal selector. The search is great, I find my link to the section of interest. Except that now the word "selector" is highlighted in bright yellow at every occurence.
Would it be easy to turn this behavior off?
Clément Pit-Claudel (Sep 29 2020 at 06:27):Sure, we can simply overwrite the corresponding CSS:
.rst-content .highlighted {
background: #F1C40F;
display: inline-block;
font-weight: bold;
padding: 0 6px;
}
Please comment on https://github.com/readthedocs/sphinx_rtd_theme/pull/876 , too
Yannick Zakowski (Oct 04 2020 at 08:41):Oops my apologies for the delay Clément, I just commented on the PR. I would be in favor of a straight up removal of highlighting, but the PR seems to suggest that there is some interest for it and that we should look for a light way to toggle/disable it instead?
Clément Pit-Claudel (Oct 05 2020 at 16:25):I think that's right
Ana de Almeida Borges (Mar 06 2022 at 18:02):As far as I can tell, there is now a way to toggle the highlighting in Sphinx 4.4.0, cf. https://github.com/sphinx-doc/sphinx/pull/9551. Can the Coq refman start using this version in order to take advantage of this feature?
Théo Zimmermann (Mar 07 2022 at 10:30):Sphinx 4.4.0 was released in 2022, so this seems a bit early to make it a hard requirement for building the documentation, but would that be sufficient if the refman that is deployed on the web is built with Sphinx 4.4.0?
Ana de Almeida Borges (Mar 07 2022 at 11:06):Yes please!
Ana de Almeida Borges (Mar 07 2022 at 11:08):I do not know whether deploying with 4.4.0 automatically shows the toggle-highlight button or whether something would need to be changed in the template, though.
Théo Zimmermann (Mar 07 2022 at 11:20):We can test this: you can open a draft PR bumping the dependency in https://github.com/coq/coq/blob/aedb9bc5f333f269cb917bc66aee45881fd72c6b/dev/ci/docker/bionic_coq/Dockerfile#L27. (Note the header comment about updating the CACHEKEY in .gitlab-ci.yml.) If this works, then we might need some more discussion about how to keep testing older Sphinx versions for compatibility preservation sake.
Ana de Almeida Borges (Mar 07 2022 at 11:45):Cool, here it is: https://github.com/coq/coq/pull/15776
Ana de Almeida Borges (Mar 07 2022 at 13:47):https://coq.gitlab.io/-/coq/-/jobs/2170712112/artifacts/_build/default/doc/refman-html/index.html
Ana de Almeida Borges (Mar 07 2022 at 13:48):I don't see a new button (I guess it was kind of asking too much that a button magically appeared). However, Search doesn't seem to be working, so I didn't manage to make some word appear highlighted.
Guillaume Melquiond (Mar 07 2022 at 15:21):Ana de Almeida Borges said:
As far as I can tell, there is now a way to toggle the highlighting in Sphinx 4.4.0, cf. https://github.com/sphinx-doc/sphinx/pull/9551. Can the Coq refman start using this version in order to take advantage of this feature?
This is not specific to Sphinx 4.4.0. For example, Why3's documentation is using Sphinx 3.4 and it already provides the button "hide search matches".
The reason Coq's documentation does not have this button is because the theme it uses purposely decided to not provide it.
As for the pull request you mention, it is not related; it is just there to remove the fragment ?highlight=foo from the URL.
Ana de Almeida Borges (Mar 07 2022 at 16:54):So basically someone already wrote a PR for the template Coq uses: https://github.com/readthedocs/sphinx_rtd_theme/pull/876
... but it doesn't seem to be going to be merged anytime soon, and I'm not sure why.
Guillaume Melquiond (Mar 07 2022 at 17:07):That is unfortunate. I think it is the worst "feature" of Coq's theme.
Guillaume Melquiond (Mar 07 2022 at 17:08):(I am purposely avoiding searching in Coq's online documentation because of it.)
Ana de Almeida Borges (Mar 07 2022 at 21:36):So Sphinx 4.5.0 (in development right now) lets one do ESC to hide the highlighting: https://github.com/sphinx-doc/sphinx/pull/9337
Ana de Almeida Borges (Mar 07 2022 at 21:37):Hopefully that is independent of the template and we can deploy the refman with Sphinx 4.5.0 and take advantage of this!
Théo Zimmermann (Mar 07 2022 at 21:47):We can also locally patch the template, but I'm not expert (I have tried something dumb and it didn't work). If you open an issue about the topic, you can cc @Clément Pit-Claudel / (cpitclaudel). Hopefully he can help.
Ana de Almeida Borges (Mar 07 2022 at 22:18):https://github.com/coq/coq/issues/15778
Ana de Almeida Borges (Jul 05 2023 at 14:03):Hi everyone, you can now use ESC to get rid of the highlights in the dev version of the refman (will be part of 8.19)! As a bonus, you can also use / as a shortcut to access the search bar.
Karl Palmskog (Jul 05 2023 at 14:03):ah, can't this be backported to 8.18? Someone could at least request inclusion...
Last updated: Sep 30 2023 at 06:01 UTC