Use <search> HTML tag instead of <div>.

[picnixz]

Fix #11701.

The use of role="search" is to ensure backward compatibility for browsers without <search> support.

cc @AA-Turner @hugovk

[jayaddison]

For reassurance: I wanted to check that the HTML <search> element should be safe in terms of backwards-compatibility. It does look backwards-compatible to me.

Explanation: W3C-spec-compliant browsers treat unknown elements as HTMLUnknownElement, and that should render in the default block-layout -- same as the div element that's being replaced.

I'm taking a quick look into CSS selectors that might rely on the div tag name. Initially the basic theme looks robust against this (a few instances of id-based lookup, where compatibility is retained).

[jayaddison]

FWIW: the agogo theme also features a role=search div.

[picnixz]

FWIW: the agogo theme also features a role=search div.

Oh thank you. I will update it as well. Maybe I should have searched the project with role="search" instead of <div id=....

(And here it's funny to see that there is neither and id nor a style).

[jayaddison]

Eventual consistency, or something like that :)

[jayaddison]

This could be worth a look: https://github.com/readthedocs/readthedocs-sphinx-search/blob/25673a35b661a6a5dbc82d26c44998028dd61cc0/sphinx_search/static/js/rtd_sphinx_search.js#L431-L448

[jayaddison]

This could be worth a look: https://github.com/readthedocs/readthedocs-sphinx-search/blob/25673a35b661a6a5dbc82d26c44998028dd61cc0/sphinx_search/static/js/rtd_sphinx_search.js#L431-L448

No matter; the comment is outdated, but readthedocs/readthedocs-sphinx-search#62 removed the expectation on a div tag name during the query.

[jayaddison]

Could however break this: https://github.com/renpy/renpy/blob/8bb5291324c7edd56a719dc4f0980e198a699b70/sphinx/source/_static/custom.css#L6