No dot completion for identifiers in most cases

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In most cases, dot autocompletion for identifiers outside of terms does not work (i.e. completion after foo.).

Steps to Reproduce

1. Type #print Bool.

Expected behavior: At this point, possible completions like Bool.and should be shown.

Actual behavior: Autocompletion interrupts, leaving only a parser error.

Versions

Lean 4.21.0-nightly-2025-05-15

Impact

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

Reproduce the problem with #print Bool. and verify that completions such as Bool.and are absent while a parser error remains. Trace the identifier completion path for code outside terms, then confirm that dot completion works in this example and does not interrupt with a parser error.