Namespace completion inserts full name rather than remainder

[tydeu]

Description

When autocompleting a namespace (e,g, Lean.PrettyPrinter) on a non-initial part (e.g., PrettyPrinter), Lean will insert the full name of the namespace at that segment (e.g., Lean.Lean.PrettyPrinter) rather than just the remainder, This only happens for namespaces, completing constants works as expected (e.g., Lean.PrettyPrinter.Unexpander).

Steps to Reproduce

#check Lean.Pretty
                --^ autocomplete here and select `Lean.PrettyPrinter`

-- Lean will auto complete like so
#check Lean.Lean.PrettyPrinter

Expected behavior:

Lean will autocomplete the name to Lean.PrettyPrinter.

Actual behavior:

Lean autocompletes the name to Lean.Lean.PrettyPrinter.

Versions

leanprover/lean4:v4.12.0 VSCode Extension v0.0.178 Windows 10 22H2

Impact

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