Stream: Coq users

Topic: refman: avoiding highlighting by default?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Clément Pit-Claudel (Oct 05 2020 at 16:25):

I think that's right

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Ana de Almeida Borges (Mar 07 2022 at 11:06):

Yes please!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Mar 07 2022 at 11:45):

Cool, here it is: https://github.com/coq/coq/pull/15776

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Mar 07 2022 at 17:07):

That is unfortunate. I think it is the worst "feature" of Coq's theme.

view this post on Zulip Guillaume Melquiond (Mar 07 2022 at 17:08):

(I am purposely avoiding searching in Coq's online documentation because of it.)

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Mar 07 2022 at 22:18):

https://github.com/coq/coq/issues/15778


Last updated: Jan 29 2023 at 06:02 UTC