All notable changes to the "Loogle Lean" extension will be documented in this file.
Check Keep a Changelog for recommendations on how to structure this file.
- Dependency updates because github flagged vulnerabilities
- Fixed the documentation link which now leads directly to the definition on the corresponding mathlib4_docs page.
- Fixed a pseudo-bug that caused no hits to appear because there were too few and they were being filtered out by the search term itself
- Added animation for searching. This is useful during long searches.
- Reorganised the code more meaningfully.
- Improved the title and placeholder of the hits and suggestions pickers.
- Added a user agent containing vscode version and extension version
- The extension tracks a query and entries in the search bar at all stages.
- Fixed UI issues with search bar which makes it disappear before the results arrive from loogle
- Fixed a bug which caused suggestions of length 1 to be silently ignored.
- Fixed some query formatting issues and responses for hits
- Fixed a URI encoding error
- There is now an option to avoid seeing module names
- Changed visible name to
Loogle Lean
- Initial release