Skip to content
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

Searching the documentation with filters #131

Open
wants to merge 37 commits into
base: master
Choose a base branch
from
Open

Searching the documentation with filters #131

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
6dbc6f0
setup branch
polibb Nov 10, 2020
3b931f6
Merge branch 'master' into search-docs
polibb Nov 22, 2020
353ff0d
Merge branch 'master' into search-docs
polibb Nov 27, 2020
c6711a7
improve code readability
polibb Dec 11, 2020
80686ab
Merge branch 'master' into search-docs
polibb Dec 11, 2020
e23988f
minor fixes
polibb Dec 19, 2020
c48b293
python script readability improvements
polibb Jan 16, 2021
6b4bfc3
Merge branch 'master' into search-docs
polibb Jan 21, 2021
7110fa7
extract data structures for readability
polibb Jan 21, 2021
ab0e46f
fix build
robertylewis Jan 21, 2021
67b7951
use class instead of dict for structure field names
robertylewis Jan 21, 2021
1228ce8
Merge pull request #1 from leanprover-community/search-docs
polibb Jan 24, 2021
67287f0
Merge pull request #2 from leanprover-community/search-docs-class
polibb Jan 24, 2021
d965133
small fixes
polibb Feb 7, 2021
ac59932
main py script structure fixes
polibb Feb 10, 2021
7341c7d
Merge branch 'search-docs' of https://github.com/pokixu/doc-gen into …
polibb Feb 10, 2021
a932deb
Merge branch 'master' into search-docs
polibb Mar 20, 2021
be8c23e
Merge branch 'master' into search-docs
polibb Mar 28, 2021
15eb701
cleanup comments
polibb Mar 28, 2021
a37d600
searchable data export structure
polibb Mar 29, 2021
ccb7abf
searchable data lists per file name
polibb Mar 29, 2021
e7f6812
data structure for searching done
polibb Apr 3, 2021
d8212ca
searchable json holds files togethere with declarations
polibb May 1, 2021
c21ebe6
Merge branch 'master' into search-docs
polibb May 3, 2021
8d4da88
building leanpkg increases commit #
polibb May 3, 2021
8dddd0a
searching through index; styling; WIP filters
polibb May 4, 2021
5432001
add filters to UI
polibb May 8, 2021
4c78d9c
show all results implementation
polibb May 11, 2021
3d52ff2
clean up and version of mathlib commits up
polibb May 12, 2021
0028904
filter searching on top of results
polibb May 14, 2021
c7a94a3
lean version reference
polibb May 14, 2021
ada2c1a
no errors on nullable elements; add loading when render all too slow
polibb May 15, 2021
8b8b257
Merge remote-tracking branch 'upstream/master'
polibb May 15, 2021
c01f230
trim query whitespace before searching
polibb May 17, 2021
14355ad
remove unnecessary files
polibb May 17, 2021
d71a7da
Change extension from .json to .bmp
gebner Jun 29, 2021
e4765ef
Merge branch 'master' into master
robertylewis Aug 12, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading