max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: tolerate more errors in server

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-01-02 14:13:03 -05:00
parent 1dd96bd004
commit 66a715dde1
No known key found for this signature in database
GPG key ID: 4E27C2EBC32B69B7
2 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Server/FileWorker.lean
View file

@ -225,9 +225,10 @@ section NotificationHandling
let oldDoc ← (←read).docRef.get
let some newVersion ← pure docId.version?
| throwServerError "Expected version number"
if newVersion <= oldDoc.meta.version then
throwServerError "Got outdated version number"
if ¬ changes.isEmpty then
if newVersion ≤ oldDoc.meta.version then
-- TODO(WN): This happens on restart sometimes.
IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
else if ¬ changes.isEmpty then
let (newDocText, minStartOff) := foldDocumentChanges changes oldDoc.meta.text
updateDocument ⟨docId.uri, newVersion, newDocText⟩ minStartOff
-- TODO(WN): cancel pending requests?

10
src/Lean/Server/Watchdog.lean
View file

@ -353,16 +353,20 @@ section MessageHandling
| "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam
| "textDocument/hover" => handle HoverParams
| "textDocument/documentSymbol" => handle DocumentSymbolParams
| _ => throwServerError s!"Got unsupported request: {method}"
| _ =>
(←read).hOut.writeLspResponseError
{ id := id
code := ErrorCode.methodNotFound
message := s!"Unsupported request method: {method}" }
def handleNotification (method : String) (params : Json) : ServerM Unit :=
def handleNotification (method : String) (params : Json) : ServerM Unit := do
let handle := (fun α [FromJson α] (handler : α → ServerM Unit) => parseParams α params >>= handler)
match method with
| "textDocument/didOpen" => handle DidOpenTextDocumentParams handleDidOpen
| "textDocument/didChange" => handle DidChangeTextDocumentParams handleDidChange
| "textDocument/didClose" => handle DidCloseTextDocumentParams handleDidClose
| "$/cancelRequest" => handle CancelParams handleCancelRequest
| _ => throwServerError "Got unsupported notification method"
| _ => (←read).hLog.putStrLn s!"Got unsupported notification: {method}"
end MessageHandling
section MainLoop