Completion popup reopens after Esc in Lean files; caused by default quickSuggestionsDelay of 200

Description

In Lean 4 files the completion popup cannot be dismissed. Pressing Esc (or Shift+Esc) closes it for about 0.1 s, then it reopens. This happens for every word, every time. Because the popup is always open, pressing Enter to start a new line accepts the top suggestion instead. For example, typing with and pressing Enter produced With, a word-based suggestion taken from a comment in the file.

The cause appears to be the extension's default "editor.quickSuggestionsDelay": 200 for [lean4]. Overriding it to VS Code's default of 10 fixes the problem completely.

Context

Found while working on tactic proofs in a small Lake project with no Mathlib dependency. No prior Zulip discussion. I searched this tracker and Zulip and found no existing report.

Steps to Reproduce

1. With default settings, open any .lean file.
2. Type any identifier or keyword so the completion popup appears.
3. Press Esc or Shift+Esc.

Expected behavior: The popup closes and stays closed until I type again.

Actual behavior: The popup closes and reopens about 0.1 s later. Repeating Esc never dismisses it. Enter then accepts the top suggestion instead of inserting a newline.

Versions

vscode-lean4 0.0.239
Lean (version 4.32.2, arm64-apple-darwin24.6.0, commit f3b06c705e6c85f5314019d5d3baab0fec5b580c, Release)
macOS 26.6 (25G72), arm64
VS Code 1.138.0

Additional Information

• Reproduces after running "Lean 4: Server: Stop Server", so the language server is not involved.

• Does not reproduce in .tex files in the same window, where Esc dismisses the popup normally.

• Workaround that fully fixes it, added to user settings:

  "[lean4]": {
    "editor.quickSuggestionsDelay": 10
  }
  

Start by locating the extension setting that assigns editor.quickSuggestionsDelay for [lean4], then reproduce the behavior in a Lean file with the default configuration. Confirm the change preserves completion while allowing Esc to dismiss the popup and Enter to insert a newline; the issue is done when the relevant regression coverage or manual verification passes.