Skip to content

feat: search box #241

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.

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

Merged
merged 40 commits into from
Jan 31, 2025
Merged

feat: search box #241

merged 40 commits into from
Jan 31, 2025

Conversation

david-christiansen
Copy link
Collaborator

Adds a search box that uses Verso's internal metadata for a live index.

@david-christiansen
Copy link
Collaborator Author

david-christiansen commented Jan 10, 2025

Requries leanprover/verso#267, but the search code is by @jakobvase

@david-christiansen david-christiansen added the HTML available HTML has been generated for this PR label Jan 10, 2025
@github-actions github-actions bot temporarily deployed to lean-ref-pr-#241 January 10, 2025 14:31 Inactive
@github-actions github-actions bot temporarily deployed to lean-ref-pr-draft-#241 January 10, 2025 14:31 Inactive
@jakobvase jakobvase added HTML available HTML has been generated for this PR and removed HTML available HTML has been generated for this PR labels Jan 12, 2025
@github-actions github-actions bot temporarily deployed to lean-ref-pr-#241 January 12, 2025 11:45 Inactive
@github-actions github-actions bot temporarily deployed to lean-ref-pr-draft-#241 January 12, 2025 11:45 Inactive
@jakobvase jakobvase added HTML available HTML has been generated for this PR and removed HTML available HTML has been generated for this PR labels Jan 12, 2025
@ashandoak
Copy link
Member

@jakobvase the live search results seem to be vertically misaligned. Looks like the term (on the left) is top justified, while the category (on the right) is bottom justified within the flex container.

Screenshot 2025-01-21 at 7 24 38 PM

@jakobvase
Copy link
Contributor

@jakobvase the live search results seem to be vertically misaligned. Looks like the term (on the left) is top justified, while the category (on the right) is bottom justified within the flex container.
Screenshot 2025-01-21 at 7 24 38 PM

Yeah that's how I wanted it to work. If you view it on mobile or a smaller screen, or if the term is long, the category is displayed below the term.

But you're right that on your screenshot it looks off. I'll see if I can improve that.

@david-christiansen
Copy link
Collaborator Author

Is it possible with the available time to additionally indicate that there were more results not in the list? Ideally the bottom might say something like "Showing 30/150 results", or potentially just "Showing the first 30 results", so that there's some indication that it was truncated? I think that the current design communicates that all the results are present, which could be really frustrating. Other than that, assuming that the spelling correction is what's turning ! into 1, I think we're good. Thanks!

This was a little complex to get to work, since it didn't show up when
navigating the search results with the keyboard, but it's working now.
@jakobvase
Copy link
Contributor

I've increased the limit to 30, removed autocorrect on ios, and added the "showing n/m results".

I see the "!" as "1" too, but only some of the time. I haven't had the time to dig into it - I can see if I have time later this week, but I don't see it as a blocker. I agree it has to be fixed soon.

@jakobvase jakobvase added HTML available HTML has been generated for this PR and removed HTML available HTML has been generated for this PR labels Jan 27, 2025
@david-christiansen david-christiansen marked this pull request as ready for review January 27, 2025 20:29
@david-christiansen
Copy link
Collaborator Author

This is much nicer! Thank you!

@jakobvase
Copy link
Contributor

I've fixed the 1/! issue. Please remember to change the toc's z-index to 9, so it doesn't look like this:
Screenshot 2025-01-29 at 17 07 04
Otherwise we're good for release from my side!

Copy link
Contributor

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit c78da68.

@david-christiansen
Copy link
Collaborator Author

OK, I think it's finally good to go. Thanks again! 🚀

@david-christiansen david-christiansen merged commit 5bb544d into main Jan 31, 2025
8 checks passed
@david-christiansen david-christiansen deleted the search-box branch January 31, 2025 22:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
HTML available HTML has been generated for this PR
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants