Lean's LSP internals appear in autocompletes for `IO.FS.Stream`

Description

When a library transitively imports the Lean language server, then various functions that it defines in the IO.FS.Stream namespace show up in completion results for streams. In fact, they make up the majority of these completion results!

This could easily hit a user who's downstream of Verso or Alloy, both of which define their own LSP handlers.

Context

This came up when working on the IO chapter of the reference manual, but it's not a blocker in the slightest.

Steps to Reproduce

1. Open a new empty Lean file and type #check IO.FS.Stream. and invoke completion.
2. Observe the completion list
3. Add import Lean as the first line of the file
4. Invoke completion in the same position as before, and observe the completion list

Expected behavior:

I would expect that the completions were unchanged.

Actual behavior:

The majority of the completions list has to do with JSON-RPC and LSP, giving the impression that this is the purpose of IO.FS.Stream.

Suggestions

I think this could be solved in two ways in the language server:

1. Get those functions out of the namespace. This would make the experience of working on the LSP server a bit worse, because dot-completion would no longer select those functions.

2. Define abbref LspStream := IO.FS.Stream and then put the functions in the LSPStream namespace. This would spare downstream users from seeing them, and also perhaps make it marginally more clear which role a given stream plays.

Versions

"4.15.0-nightly-2024-11-19", on live.lean-lang.org.

Impact

I think this is a papercut at worst.

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

Reproduce the completion difference for IO.FS.Stream. in an empty file with and without import Lean. Read the IO.FS.Stream namespace and the Lean language-server LSP definitions, then determine how the LSP functions can be separated from downstream stream completions. Done means the completion list no longer presents JSON-RPC and LSP functions as the majority of IO.FS.Stream results.