diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean index b943b16c0a..a2a3e7729e 100644 --- a/src/Lean/Server/AsyncList.lean +++ b/src/Lean/Server/AsyncList.lean @@ -104,7 +104,7 @@ where let tasks : { t : List _ // t.length > 0 } := match cancelTk? with | none => ⟨[tl, timeoutTask], by exact Nat.zero_lt_succ _⟩ - | some cancelTk => ⟨[cancelTk, tl, timeoutTask], by exact Nat.zero_lt_succ _⟩ + | some cancelTk => ⟨[tl, cancelTk, timeoutTask], by exact Nat.zero_lt_succ _⟩ let r ← ServerTask.waitAny tasks.val (h := tasks.property) match r with | .inl _ => return ⟨[], none, false⟩ -- Timeout or cancellation - stop waiting diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index aa370b17a3..fab55b498d 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -534,22 +534,21 @@ section NotificationHandling let oldDoc := (←get).doc let cancelTk ← RequestCancellationToken.new let newVersion := docId.version?.getD 0 - let _ ← ServerTask.IO.mapTaskCostly (t := st.srcSearchPathTask) fun srcSearchPath => - let rc : RequestContext := - { rpcSessions := st.rpcSessions - srcSearchPath - doc := oldDoc - cancelTk - hLog := ctx.hLog - initParams := ctx.initParams } - RequestM.runInIO (handleOnDidChange p) rc + let rc : RequestContext := { + rpcSessions := st.rpcSessions + srcSearchPathTask := st.srcSearchPathTask + doc := oldDoc + cancelTk + hLog := ctx.hLog + initParams := ctx.initParams + } + RequestM.runInIO (handleOnDidChange p) rc if ¬ changes.isEmpty then let newDocText := foldDocumentChanges changes oldDoc.meta.text updateDocument ⟨docId.uri, newVersion, newDocText, oldDoc.meta.dependencyBuildMode⟩ for (_, r) in st.pendingRequests do r.cancelTk.cancelByEdit - def handleCancelRequest (p : CancelParams) : WorkerM Unit := do let st ← get let some r := st.pendingRequests.find? p.id @@ -728,32 +727,30 @@ section MessageHandling return let cancelTk ← RequestCancellationToken.new - -- we assume that any other request requires at least the search path -- TODO: move into language-specific request handling - let requestTask ← ServerTask.IO.bindTaskCheap st.srcSearchPathTask fun srcSearchPath => do - let rc : RequestContext := - { rpcSessions := st.rpcSessions - srcSearchPath - doc := st.doc - cancelTk - hLog := ctx.hLog - initParams := ctx.initParams } - let t? ← EIO.toIO' <| handleLspRequest method params rc - match t? with + let rc : RequestContext := + { rpcSessions := st.rpcSessions + srcSearchPathTask := st.srcSearchPathTask + doc := st.doc + cancelTk + hLog := ctx.hLog + initParams := ctx.initParams } + let requestTask? ← EIO.toIO' <| handleLspRequest method params rc + let requestTask ← match requestTask? with + | Except.error e => + emitResponse ctx (isComplete := false) <| e.toLspResponseError id + pure <| ServerTask.pure <| .ok () + | Except.ok requestTask => ServerTask.IO.mapTaskCheap (t := requestTask) fun + | Except.ok r => do + if ← cancelTk.wasCancelledByCancelRequest then + -- Try not to emit a partial response if this request was cancelled. + -- Clients usually discard responses for requests that they cancelled anyways, + -- but it's still good to send less over the wire in this case. + emitResponse ctx (isComplete := false) <| RequestError.requestCancelled.toLspResponseError id + return + emitResponse ctx (isComplete := r.isComplete) <| .response id (toJson r.response) | Except.error e => - emitResponse ctx (isComplete := false) <| e.toLspResponseError id - pure <| ServerTask.pure <| .ok () - | Except.ok t => ServerTask.IO.mapTaskCheap (t := t) fun - | Except.ok r => do - if ← cancelTk.wasCancelledByCancelRequest then - -- Try not to emit a partial response if this request was cancelled. - -- Clients usually discard responses for requests that they cancelled anyways, - -- but it's still good to send less over the wire in this case. - emitResponse ctx (isComplete := false) <| RequestError.requestCancelled.toLspResponseError id - return - emitResponse ctx (isComplete := r.isComplete) <| .response id (toJson r.response) - | Except.error e => - emitResponse ctx (isComplete := false) <| e.toLspResponseError id + emitResponse ctx (isComplete := false) <| e.toLspResponseError id queueRequest id { cancelTk, requestTask } where diff --git a/src/Lean/Server/FileWorker/InlayHints.lean b/src/Lean/Server/FileWorker/InlayHints.lean index 5d32135439..75eb75bf11 100644 --- a/src/Lean/Server/FileWorker/InlayHints.lean +++ b/src/Lean/Server/FileWorker/InlayHints.lean @@ -126,12 +126,10 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) : let timeSinceLastEditMs := timestamp - lastEditTimestamp inlayHintEditDelayMs - timeSinceLastEditMs let (snaps, _, isComplete) ← ctx.doc.cmdSnaps.getFinishedPrefixWithConsistentLatency editDelayMs.toUInt32 (cancelTk? := ctx.cancelTk.cancellationTask) - -- This cancellation check is crucial for the invariant `finishedSnaps >= oldFinishedSnaps` below. - RequestM.checkCancelled let snaps := snaps.toArray let finishedSnaps := snaps.size let oldFinishedSnaps := s.oldFinishedSnaps - -- File processing is monotonic modulo `didChange` notifications and cancellation. + -- File processing is monotonic modulo `didChange` notifications. assert! finishedSnaps >= oldFinishedSnaps -- VS Code emits inlay hint requests *every time the user scrolls*. This is reasonably expensive, -- so in addition to re-using old inlay hints from parts of the file that haven't been processed @@ -165,55 +163,65 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) : def handleInlayHintsDidChange (p : DidChangeTextDocumentParams) : StateT InlayHintState RequestM Unit := do - let meta := (← read).doc.meta - let text := meta.text - let srcSearchPath := (← read).srcSearchPath - let .ok modName? ← EIO.toBaseIO <| do - let some path := System.Uri.fileUriToPath? meta.uri - | return none - let some mod ← searchModuleNameOfFileName path srcSearchPath - | return some <| ← moduleNameOfFileName path none - return some mod - | return - let modName := modName?.getD .anonymous -- `.anonymous` occurs in untitled files let s ← get - let mut updatedOldInlayHints := #[] - for ihi in s.oldInlayHints do - let mut ihi := ihi - let mut inlayHintInvalidated := false - for c in p.contentChanges do - let .rangeChange changeRange newText := c - | set <| { s with oldInlayHints := #[] } -- `fullChange` => all old inlay hints invalidated - return - let changeRange := text.lspRangeToUtf8Range changeRange - let some ihi' := applyEditToHint? modName ihi changeRange newText - | -- Change in some position of inlay hint => inlay hint invalidated - inlayHintInvalidated := true - break - ihi := ihi' - if ! inlayHintInvalidated then - updatedOldInlayHints := updatedOldInlayHints.push ihi - let isInlayHintInsertionEdit := p.contentChanges.all fun c => Id.run do - let .rangeChange changeRange newText := c - | return false - let changeRange := text.lspRangeToUtf8Range changeRange - let edit := ⟨changeRange, newText⟩ - return s.oldInlayHints.any (·.textEdits.contains edit) - let timestamp ← IO.monoMsNow - let lastEditTimestamp? := - if isInlayHintInsertionEdit then - -- For some stupid reason, VS Code doesn't remove the inlay hint when applying it, so we - -- try to figure out whether the edit was an insertion of an inlay hint and then respond - -- to the request without latency so that it inserted ASAP. - none - else - some timestamp + let updatedOldInlayHints ← updateOldInlayHints s.oldInlayHints + let lastEditTimestamp? ← determineLastEditTimestamp? s.oldInlayHints set <| { s with oldInlayHints := updatedOldInlayHints oldFinishedSnaps := 0 lastEditTimestamp? } +where + + updateOldInlayHints (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Array Elab.InlayHintInfo) := do + let meta := (← read).doc.meta + let text := meta.text + let srcSearchPath := (← read).srcSearchPath + let modName? ← EIO.toBaseIO <| do + let some path := System.Uri.fileUriToPath? meta.uri + | return none + let some mod ← searchModuleNameOfFileName path srcSearchPath + | return some <| ← moduleNameOfFileName path none + return some mod + let modName ← match modName? with + | .ok (some modName) => pure modName + | .ok none => pure .anonymous -- `.anonymous` occurs in untitled files + | .error err => throw <| .ofIoError err + let mut updatedOldInlayHints := #[] + for ihi in oldInlayHints do + let mut ihi := ihi + let mut inlayHintInvalidated := false + for c in p.contentChanges do + let .rangeChange changeRange newText := c + | return #[] -- `fullChange` => all old inlay hints invalidated + let changeRange := text.lspRangeToUtf8Range changeRange + let some ihi' := applyEditToHint? modName ihi changeRange newText + | -- Change in some position of inlay hint => inlay hint invalidated + inlayHintInvalidated := true + break + ihi := ihi' + if ! inlayHintInvalidated then + updatedOldInlayHints := updatedOldInlayHints.push ihi + return updatedOldInlayHints + + determineLastEditTimestamp? (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Option Nat) := do + let text := (← read).doc.meta.text + let isInlayHintInsertionEdit := p.contentChanges.all fun c => Id.run do + let .rangeChange changeRange newText := c + | return false + let changeRange := text.lspRangeToUtf8Range changeRange + let edit := ⟨changeRange, newText⟩ + return oldInlayHints.any (·.textEdits.contains edit) + let timestamp ← IO.monoMsNow + if isInlayHintInsertionEdit then + -- For some stupid reason, VS Code doesn't remove the inlay hint when applying it, so we + -- try to figure out whether the edit was an insertion of an inlay hint and then respond + -- to the request without latency so that it inserted ASAP. + return none + else + return some timestamp + builtin_initialize registerPartialStatefulLspRequestHandler "textDocument/inlayHint" diff --git a/src/Lean/Server/RequestCancellation.lean b/src/Lean/Server/RequestCancellation.lean index 72f68d1422..29f01c85ae 100644 --- a/src/Lean/Server/RequestCancellation.lean +++ b/src/Lean/Server/RequestCancellation.lean @@ -15,28 +15,28 @@ structure RequestCancellationToken where namespace RequestCancellationToken -def new : IO RequestCancellationToken := do +def new : BaseIO RequestCancellationToken := do return { cancelledByCancelRequest := ← IO.mkRef false cancelledByEdit := ← IO.mkRef false cancellationPromise := ← IO.Promise.new } -def cancelByCancelRequest (tk : RequestCancellationToken) : IO Unit := do +def cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit := do tk.cancelledByCancelRequest.set true tk.cancellationPromise.resolve () -def cancelByEdit (tk : RequestCancellationToken) : IO Unit := do +def cancelByEdit (tk : RequestCancellationToken) : BaseIO Unit := do tk.cancelledByEdit.set true tk.cancellationPromise.resolve () def cancellationTask (tk : RequestCancellationToken) : Task Unit := tk.cancellationPromise.result! -def wasCancelledByCancelRequest (tk : RequestCancellationToken) : IO Bool := +def wasCancelledByCancelRequest (tk : RequestCancellationToken) : BaseIO Bool := tk.cancelledByCancelRequest.get -def wasCancelledByEdit (tk : RequestCancellationToken) : IO Bool := do +def wasCancelledByEdit (tk : RequestCancellationToken) : BaseIO Bool := do tk.cancelledByEdit.get end RequestCancellationToken @@ -56,7 +56,7 @@ def CancellableM.run (tk : RequestCancellationToken) (x : CancellableM α) : IO (Except RequestCancellation α) := CancellableT.run tk x -def CancellableT.checkCancelled [Monad m] [MonadLiftT IO m] : CancellableT m Unit := do +def CancellableT.checkCancelled [Monad m] [MonadLiftT BaseIO m] : CancellableT m Unit := do let tk ← read if ← tk.wasCancelledByCancelRequest then throw .requestCancelled @@ -70,7 +70,7 @@ class MonadCancellable (m : Type → Type v) where instance (m n) [MonadLift m n] [MonadCancellable m] : MonadCancellable n where checkCancelled := liftM (MonadCancellable.checkCancelled : m PUnit) -instance [Monad m] [MonadLiftT IO m] : MonadCancellable (CancellableT m) where +instance [Monad m] [MonadLiftT BaseIO m] : MonadCancellable (CancellableT m) where checkCancelled := CancellableT.checkCancelled def RequestCancellation.check [MonadCancellable m] : m Unit := diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 0b825e96ca..223dde1dfd 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -137,12 +137,15 @@ def parseRequestParams (paramType : Type) [FromJson paramType] (params : Json) message := s!"Cannot parse request params: {params.compress}\n{inner}" } structure RequestContext where - rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare - srcSearchPath : SearchPath - doc : FileWorker.EditableDocument - hLog : IO.FS.Stream - initParams : Lsp.InitializeParams - cancelTk : RequestCancellationToken + rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare + srcSearchPathTask : ServerTask SearchPath + doc : FileWorker.EditableDocument + hLog : IO.FS.Stream + initParams : Lsp.InitializeParams + cancelTk : RequestCancellationToken + +def RequestContext.srcSearchPath (rc : RequestContext) : SearchPath := + rc.srcSearchPathTask.get abbrev RequestTask α := ServerTask (Except RequestError α) abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m