Autocomplete suggestions after dot (".") not appearing in some contexts

[LacombeJ]

Description

When typing in "." after a type or namespace in match and some tactics, the autocomplete suggestions are not appearing.

Context

I have noticed it in:

• Match expressions (in the terms right after the "|" guards)
• Tactic mode (in "apply" expressions or in "cases" guards)

Steps to Reproduce

Match Expression

1. Start with empty file (.lean) file in a lean/lake project
2. Add the following code:

inductive Direction where
  | up
  | right
  | down
  | left
deriving Repr

def angle (d: Direction) :=
  match d with
  | Direction.up => 90
  | Direction.right => 0
  | Direction.down => 270
  | Direction.left => 180

3. Delete the ".up" and try re-adding a period "." after Direction

Expected behavior:
I expect to see the same dropdown that appears after typing the dot in #eval Direction.

Actual behavior:
No suggestions dropdown, red squiggly error line appears under text and hovering shows "invalid pattern Lean 4"

Versions

VS Code Extension: v0.0.176
Lean: version 4.10.0, x86_64-w64-windows-gnu, commit c375e19, Release
OS: Windows 10

Additional Information

Similar issue found in all of the "." operators in this example

example : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
  intro h
  cases h with
  | inl hp => apply And.intro (Or.intro_left q hp) (Or.intro_left r hp)
  | inr hqr => apply And.intro (Or.intro_right p hqr.left) (Or.intro_right p hqr.right)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.