Question: How does the Lean LSP server determine whether a file is open?

[LAWArthur]

After initialization I sent the textDocument/didOpen request and got the textDocument/publishDiagnostics feedback, so I believe the file's worker has been launched properly. However when I then send a $/lean/rpc/connect request with the exactly same uri, the server replies with ContentModified: Cannot process request to closed file. I've tried delaying or repeating the request but its all the same.

After searching in the source code, I think this error is thrown by lean4/src/Lean/Server
/Watchdog.lean: forwardRequestToWorker, which uses findFileWorker to check whether file is open. But in handleDidOpen above, startFileWorker is already invoked, so the error makes me confused.

My present guess is that the didOpen request in lean has different specification from the standard LSP(which I follows), like how to convert TextDocument to FileSource I see in the code. But I can't figure it out in the source code or in the vscode Lean4 extension implementation. Do you have any suggestion on how to set up the communication properly?

[LAWArthur]

I've fixed it. It seems that lean server automatically converts windows path uri to lowercase yet doesn't do the same to uris of incoming requests. Thanks to your awesome project anyway.