search

sphinx-doc / sphinx

The Sphinx documentation generator
https://www.sphinx-doc.org/
Other
6.63k stars 2.13k forks source link

Search sections #4711

Open PatrickMassot opened 6 years ago

PatrickMassot commented 6 years ago

Problem

Procedure to reproduce the problem

Go to https://leanprover.github.io/theorem_proving_in_lean/ search for calc

Error logs / results

Build says

Running Sphinx v1.7.1
making output directory...
loading pickled environment... not yet created
building [mo]: targets for 0 po files that are out of date
building [html]: targets for 12 source files that are out of date
updating environment: 12 added, 0 changed, 0 removed
reading sources... [100%] type_classes                                                                 
looking for now-outdated files... none found
pickling environment... done
checking consistency... done
preparing documents... done
writing output... [100%] type_classes                                                                  
generating indices... genindex
writing additional pages... search
copying static files... done
copying extra files... done
dumping search index in English (code: en) ... done
dumping object inventory... done
build succeeded.

The HTML pages are in _build/html.

Expected results

I expected to see a link to https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#calculational-proofs which contains a lot of occurrences of the searched word calc. However each occurrence is inside a code block, I guess that could be the issue.

Reproducible project

Environment info

The online version linked to above is using Sphinx 1.6.3 but I check locally with the latest release 1.7.1

tk0miya commented 6 years ago

I guess you'd like to search sections. But, in current implementation, the Sphinx search is based on document, not section. The search result already contains "4. Quantifiers and Equality" document. So I think this is feature enhancement. Is my understanding right?

PatrickMassot commented 6 years ago

Sorry, I could swear the section did not appear in the results but you are right: it's because it's a section inside a web page. Indeed it would be an enhancement to display sections in the search result page, but there is no bug.