Skip to content

Sorry is invalid, hint is incorrect, isBusy flag properly resets. #334

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

Open
GitLuckier wants to merge 10 commits into
base: mapping
Choose a base branch
from
Open

Sorry is invalid, hint is incorrect, isBusy flag properly resets. #334

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
75e5cdd
Made sorry and hint be invalid rather than correct
GitLuckier Mar 30, 2026
37ed8e2
made sure hint is marked as incorrect like help
GitLuckier Mar 30, 2026
fb001d7
added unit tests for getInputArea to ensure that the blocks are order…
GitLuckier Mar 30, 2026
8102fe2
bettere tests
GitLuckier Mar 30, 2026
0e565d5
Simplified implementation
GitLuckier Mar 31, 2026
2382184
fix: bug where sometimes the `isBusy` flag would get stuck at true
GitLuckier Apr 7, 2026
f589ada
fixed out-dated tests
GitLuckier Apr 7, 2026
5c34e8c
added extra check if the DiagnosticSeverity is a warning and replaced…
GitLuckier Apr 12, 2026
4851597
fix: replaced exact string matching with more robust prefix matching
GitLuckier Apr 13, 2026
68a2662
added a few clarifying comments in the test file
GitLuckier Apr 14, 2026
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
198 changes: 0 additions & 198 deletions __tests__/lsp-client/lean/client.determineProofStatus.test.ts
View file
Open in desktop

This file was deleted.

Loading