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.

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

fix: don't use info nodes before cursor for completion #3778

Merged
merged 5 commits into from
Apr 2, 2024

Conversation

mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Mar 26, 2024

This fixes an issue where the completion would use info nodes before the cursor for computing completions.

Fixes #3462.

ToDo:

  • Fix test failures for completions that previously worked by accident (cc: @Kha)
  • stage0 update

@mhuisi mhuisi requested review from Kha and kim-em as code owners March 27, 2024 15:21
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 27, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 27, 2024

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e8a2786d6d4defa29f8991eb03e1dd975311e5ae --onto 4c0106d757d4d6d3b7f3903611ce22100d539d2a. (2024-03-27 15:45:03)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 70924be89c3aa7eee7dd0e115bf3b9df2d96eb78 --onto b4caee80a3dfc5c9619d88b16c40cc3db90da4e2. (2024-03-27 17:40:14)

@mhuisi mhuisi force-pushed the mhuisi/accidental-keyword-completion branch from b6332c7 to 594366f Compare March 27, 2024 17:22
@Kha Kha force-pushed the mhuisi/accidental-keyword-completion branch from 594366f to 630f1d0 Compare April 2, 2024 08:31
@Kha Kha enabled auto-merge April 2, 2024 08:31
@Kha Kha added this pull request to the merge queue Apr 2, 2024
Merged via the queue into leanprover:master with commit ecf0459 Apr 2, 2024
10 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Auto-complete offered after match … with
3 participants