Add multi folder support

[lovettchris]

See in this vscode multi-server sample and see: https://github.com/microsoft/vscode/wiki/Adopting-Multi-Root-Workspace-APIs

Here's a screenshot showing a multi-folder workspace open with 2 different versions of lean specified in the lean-toolchain of each folder. It fires up 2 different lean --server instances, one for each folder, and seamlessly switches between them as you edit files from each folder. The InfoView expects an "active client changed" event and "reconnects" that client to the infoview as the user switches between active workspaces.

Here's the process tree you will see for serving both these workspaces, 2 lean --servers with their separate workers.

[gebner]

I don't think the explicit LSP-client-switching is a good idea, because then the infoview only has access to one client. If you use the pin functionality then you should be able to interact with the pin even if it is from another workspace folder.

Instead we should route the LSP requests (and notification subscriptions) depending on the document URI. That is, if the infoview makes an LSP request, we look at the the URI (which should maybe become an explicit argument of sendClientNotification and co.) and then send it to the responsible LSP server. And the serverRestarted event should probably send all connected servers then.

The current version of the PR also seems to open every file in all LSP servers:

  │       ├─lean,1755034 --server /home/gebner/mathlib4
  │       │   ├─lean,1755105 --worker file:///home/gebner/mathlib4/Mathlib/Data/UnionFind.lean
  │       │   ├─lean,1755179 --worker file:///home/gebner/mathport/Mathport/Syntax/Data4.lean
  │       │   ├─lean,1758529 --worker file:///home/gebner/mathport/Mathport/Syntax/Parse.lean
  │       │   ├─lean,1759169 --worker file:///home/gebner/mathlib4/Mathlib/Data/Nat/Gcd.lean
  │       │   └─lean,1759410 --worker file:///home/gebner/mathport/Mathport/Syntax/Translate.lean
  │       └─lean,1755184 --server /home/gebner/mathport
  │           ├─lean,1757491 --worker file:///home/gebner/mathlib4/Mathlib/Data/UnionFind.lean
  │           ├─lean,1759171 --worker file:///home/gebner/mathlib4/Mathlib/Data/Nat/Gcd.lean
  │           └─lean,1759408 --worker file:///home/gebner/mathport/Mathport/Syntax/Translate.lean

[lovettchris]

@gebner , thanks for the bug report, I suspect I have to filter out sendNotification calls for files opened in a different workspace now, see this commit. Here's the process tree which shows it is no longer opening every file in every client:

cmd.exe: C:\WINDOWS\system32\cmd.exe /d /s /c "lean --server d:\Temp\lean_examples\Foo"
      lean.exe: lean  --server d:\Temp\lean_examples\Foo
        lean.exe: "C:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2021-12-28\bin\lean.exe" --server d:\Temp\lean_examples\Foo
          lean.exe: c:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2021-12-28\bin\lean.exe "--worker" "file:///d%3A/Temp/lean_examples/Foo/Main.lean"
    cmd.exe: C:\WINDOWS\system32\cmd.exe /d /s /c "lean --server d:\Temp\lean_examples\test"
      lean.exe: lean  --server d:\Temp\lean_examples\test
        lean.exe: "C:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2022-01-20\bin\lean.exe" --server d:\Temp\lean_examples\test
          lean.exe: c:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly-2022-01-20\bin\lean.exe "--worker" "file:///d%3A/Temp/lean_examples/test/Test.lean"

[lovettchris]

@gebner Instead we should route the LSP requests (and notification subscriptions) depending on the document URI. That is, if the infoview makes an LSP request, we look at the the URI (which should maybe become an explicit argument of sendClientNotification and co.) and then send it to the responsible LSP server. And the serverRestarted event should probably send all connected servers then.

Done. See InfoView is now mult-client aware. lean4.restartServer still only restarts the client associated with the active document you are editing, but that's easy to change if we want.

[gebner]

Great!