diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 53b4d06a3c8b..36af9402276d 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -440,7 +440,7 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => throw <| IO.userError (← msg.toString)
-  | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
+  | Except.error (Exception.internal id _) => throw <| IO.userError (← id.getDescription)
   | Except.ok a                            => return a
 
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index fac66dd4731c..836aa4afd406 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -63,7 +63,7 @@ inductive ErrorCode where
   If a client decides that a result is not of any use anymore
   the client should cancel the request. -/
   | contentModified
-  /-- The client has canceled a request and a server as detected the cancel. -/
+  /-- The client has cancelled a request and the server has detected the cancel. -/
   | requestCancelled
   -- Lean-specific codes below.
   | rpcNeedsReconnect
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index e8f915fe8423..f521f7ed8357 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -492,7 +492,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     hasNoErrorMessages
   catch
     | ex@(Exception.error _ _) => do logException ex; pure false
-    | Exception.internal id _  => do logError (← id.getName); pure false
+    | Exception.internal id _  => do logError (← id.getDescription); pure false
   finally
     restoreMessages prevMessages
   if succeeded then
diff --git a/src/Lean/Elab/DocString/Builtin.lean b/src/Lean/Elab/DocString/Builtin.lean
index a4a9daa857fb..a9baec1810db 100644
--- a/src/Lean/Elab/DocString/Builtin.lean
+++ b/src/Lean/Elab/DocString/Builtin.lean
@@ -786,7 +786,7 @@ instance : Append DocCode where
 
 
 private partial def highlightSyntax
-    [Monad m] [MonadLiftT IO m]
+    [Monad m] [MonadLiftT (EIO Exception) m]
     (trees : PersistentArray InfoTree) (stx : Syntax) : m DocCode := do
   (go stx).run {} <&> (·.2)
 where
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 4e78cabde4d6..cdb771caa70d 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -113,8 +113,9 @@ def InfoState.substituteLazy (s : InfoState) : Task InfoState :=
     lazyAssignment := {}
   }
 
-/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`. -/
-def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
+/-- Embeds a `CoreM` action in `EIO` by supplying the information stored in `info`. -/
+def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α)
+    (cancelTk? : Option IO.CancelToken := none) : EIO Exception α := do
   -- We assume that this function is used only outside elaboration, mostly in the language server,
   -- and so we can and should provide access to information regardless whether it is exported.
   let env := info.env.setExporting false
@@ -122,20 +123,22 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     We must execute `x` using the `ngen` stored in `info`. Otherwise, we may create `MVarId`s and `FVarId`s that
     have been used in `lctx` and `info.mctx`.
   -/
-  (·.1) <$>
-    (withOptions (fun _ => info.options) x).toIO
-      { currNamespace := info.currNamespace, openDecls := info.openDecls
-        fileName := "<InfoTree>", fileMap := default }
-      { env, ngen := info.ngen }
+  (withOptions (fun _ => info.options) x).run'
+    { currNamespace := info.currNamespace, openDecls := info.openDecls
+      fileName := "<InfoTree>", fileMap := default, cancelTk? }
+    { env, ngen := info.ngen }
 
-def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
-  (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })
+def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α)
+    (cancelTk? : Option IO.CancelToken := none) :
+    EIO Exception α := do
+  info.runCoreM (x.run' { lctx := lctx } { mctx := info.mctx }) cancelTk?
 
 def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext :=
   { env  := info.env, mctx := info.mctx, lctx := lctx,
     opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
 
-def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
+def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) :
+    BaseIO Format :=
   ppTerm (info.toPPContext lctx) ⟨stx⟩  -- HACK: might not be a term
 
 private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format :=
@@ -155,10 +158,10 @@ private def formatElabInfo (ctx : ContextInfo) (info : ElabInfo) : Format :=
   else
     f!"{formatStxRange ctx info.stx} @ {info.elaborator}"
 
-def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α :=
+def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : EIO Exception α :=
   ctx.runMetaM info.lctx x
 
-def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
+def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : EIO Exception Format := do
   info.runMetaM ctx do
     let ty : Format ←
       try
@@ -170,39 +173,39 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
 def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
   f!"[PartialTerm] @ {formatElabInfo ctx info.toElabInfo}"
 
-def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
+def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : EIO Exception Format :=
   match info with
   | .dot i (expectedType? := expectedType?) .. => return f!"[Completion-Dot] {← i.format ctx} : {expectedType?}"
   | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[Completion-Id] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
   | _ => return f!"[Completion] {info.stx} @ {formatStxRange ctx info.stx}"
 
-def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
-  return f!"[Command] @ {formatElabInfo ctx info.toElabInfo}"
+def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : Format :=
+  f!"[Command] @ {formatElabInfo ctx info.toElabInfo}"
 
-def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : IO Format := do
-  return f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}"
+def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : Format :=
+  f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}"
 
-def ErrorNameInfo.format (ctx : ContextInfo) (info : ErrorNameInfo) : IO Format := do
-  return f!"[ErrorName] {info.errorName} @ {formatStxRange ctx info.stx}"
+def ErrorNameInfo.format (ctx : ContextInfo) (info : ErrorNameInfo) : Format :=
+  f!"[ErrorName] {info.errorName} @ {formatStxRange ctx info.stx}"
 
-def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
+def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : EIO Exception Format := do
   ctx.runMetaM info.lctx do
     return f!"[Field] {info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}"
 
-def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format :=
+def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : EIO Exception Format :=
   if goals.isEmpty then
     return "no goals"
   else
     ctx.runMetaM {} (return Std.Format.prefixJoin "\n" (← goals.mapM (Meta.ppGoal ·)))
 
-def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
+def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : EIO Exception Format := do
   let ctxB := { ctx with mctx := info.mctxBefore }
   let ctxA := { ctx with mctx := info.mctxAfter }
   let goalsBefore ← ctxB.ppGoals info.goalsBefore
   let goalsAfter  ← ctxA.ppGoals info.goalsAfter
   return f!"[Tactic] @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
-def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
+def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : BaseIO Format := do
   let stx    ← ctx.ppSyntax info.lctx info.stx
   let output ← ctx.ppSyntax info.lctx info.output
   return f!"[MacroExpansion]\n{stx}\n===>\n{output}"
@@ -216,16 +219,16 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"[FieldRedecl] @ {formatStxRange ctx info.stx}"
 
-def DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) : IO (Option String) := do
+def DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) :
+    BaseIO (Option String) := do
   match info.mkDocString? with
   | none => return none
   | some act =>
-    try
-      act ppCtx
-    catch ex =>
-      return s!"[Error: {ex.toString}]"
+    match ← (act ppCtx).toBaseIO with
+    | .ok v => return v
+    | .error ex => return s!"[Error: {ex.toString}]"
 
-def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
+def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : EIO Exception Format := do
   let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
   let docString? ← info.docString? (ctx.toPPContext info.lctx)
   return f!"[DelabTerm] @ {← TermInfo.format ctx info.toTermInfo}\n\
@@ -242,14 +245,14 @@ def DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format :=
 def DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format :=
   f!"[DocElab] {info.name} ({repr info.kind}) @ {formatElabInfo ctx info.toElabInfo}"
 
-def Info.format (ctx : ContextInfo) : Info → IO Format
+def Info.format (ctx : ContextInfo) : Info → EIO Exception Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
   | ofPartialTermInfo i    => pure <| i.format ctx
-  | ofCommandInfo i        => i.format ctx
+  | ofCommandInfo i        => pure <| i.format ctx
   | ofMacroExpansionInfo i => i.format ctx
-  | ofOptionInfo i         => i.format ctx
-  | ofErrorNameInfo i      => i.format ctx
+  | ofOptionInfo i         => pure <| i.format ctx
+  | ofErrorNameInfo i      => pure <| i.format ctx
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
   | ofUserWidgetInfo i     => pure <| i.format
@@ -304,7 +307,8 @@ def PartialContextInfo.format (ctx : PartialContextInfo) : Format :=
   | .parentDeclCtx n => s!"parent[{n}]"
   | .autoImplicitCtx implicits => s!"autoImplicits[{implicits}]"
 
-partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format := do
+partial def InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) :
+    EIO Exception Format := do
   match tree with
   | hole id     => return .nestD f!"• ?{toString id.name}"
   | context i t => format t <| i.mergeIntoOuter? ctx?
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 73162ffa9085..fa91832e43d7 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -237,8 +237,7 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [
   | Exception.error ref msg => logErrorAt ref msg
   | Exception.internal id _ =>
     unless isAbortExceptionId id || ex.isInterrupt do
-      let name ← id.getName
-      logError m!"internal exception: {name}"
+      logError (← id.getDescription)
 
 /--
 If `x` throws an exception, catch it and turn it into a log message (using `logException`).
diff --git a/src/Lean/InternalExceptionId.lean b/src/Lean/InternalExceptionId.lean
index 6b17afbf7036..56ac4bd10242 100644
--- a/src/Lean/InternalExceptionId.lean
+++ b/src/Lean/InternalExceptionId.lean
@@ -47,4 +47,8 @@ def InternalExceptionId.getName (id : InternalExceptionId) : IO Name :=  do
   else
     throw <| IO.userError "invalid internal exception id"
 
+/-- Return a description containing the internal exception's name. -/
+def InternalExceptionId.getDescription (id : InternalExceptionId) : IO String :=
+  return s!"internal exception: {← id.getName}"
+
 end Lean
diff --git a/src/Lean/Linter/List.lean b/src/Lean/Linter/List.lean
index 1e99ef66b454..9fcbd8d09582 100644
--- a/src/Lean/Linter/List.lean
+++ b/src/Lean/Linter/List.lean
@@ -207,7 +207,8 @@ def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"
 def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]
 
 /-- Find all binders appearing in the given info tree. -/
-def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Syntax × Name × Expr)) :=
+def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) :
+    EIO Exception (List (Syntax × Name × Expr)) :=
   t.collectTermInfoM fun ctx ti => do
     if ti.isBinder then do
       -- Something is wrong here: sometimes `inferType` fails with an unknown fvar error,
diff --git a/src/Lean/Server/CodeActions/UnknownIdentifier.lean b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
index bdbf4f1145dc..e8ae5fd37b17 100644
--- a/src/Lean/Server/CodeActions/UnknownIdentifier.lean
+++ b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
@@ -137,7 +137,7 @@ def computeDotQuery?
     (doc : EditableDocument)
     (ctx : Elab.ContextInfo)
     (ti : Elab.TermInfo)
-    : IO (Option Query) := do
+    : EIO Exception (Option Query) := do
   let text := doc.meta.text
   let some pos := ti.stx.getPos? (canonicalOnly := true)
     | return none
@@ -173,7 +173,7 @@ def computeDotIdQuery?
     (id : Name)
     (lctx : LocalContext)
     (expectedType? : Option Expr)
-    : IO (Option Query) := do
+    : EIO Exception (Option Query) := do
   let some pos := stx.getPos? (canonicalOnly := true)
     | return none
   let some tailPos := stx.getTailPos? (canonicalOnly := true)
@@ -277,6 +277,7 @@ def handleUnknownIdentifierCodeAction
   }
   let r ← ServerTask.waitAny [
     responseTask.mapCheap Sum.inl,
+    -- TODO: does this intentionally ignore edit-based cancellations?
     rc.cancelTk.requestCancellationTask.mapCheap Sum.inr
   ]
   let .inl (.success response) := r
diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean
index db21662deb6d..2f1b136be2aa 100644
--- a/src/Lean/Server/Completion/CompletionCollectors.lean
+++ b/src/Lean/Server/Completion/CompletionCollectors.lean
@@ -542,7 +542,7 @@ def optionCompletion
     (ctx               : ContextInfo)
     (stx               : Syntax)
     (caps              : ClientCapabilities)
-    : IO (Array ResolvableCompletionItem) :=
+    : EIO Exception (Array ResolvableCompletionItem) :=
   ctx.runMetaM {} do
     -- HACK(WN): unfold the type so ForIn works
     let (decls : Std.TreeMap _ _ _) ← getOptionDecls
@@ -569,7 +569,7 @@ def errorNameCompletion
     (ctx               : ContextInfo)
     (partialId         : Syntax)
     (caps              : ClientCapabilities)
-    : IO (Array ResolvableCompletionItem) :=
+    : EIO Exception (Array ResolvableCompletionItem) :=
   ctx.runMetaM {} do
     let explanations ← getErrorExplanations
     return trailingDotCompletion explanations partialId caps ctx fun name explan textEdit? => {
@@ -596,7 +596,7 @@ def tacticCompletion
     (pos               : Lsp.Position)
     (completionInfoPos : Nat)
     (ctx               : ContextInfo)
-    : IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
+    : EIO Exception (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
   -- Don't include tactics that are identified only by their internal parser name
   let allTacticDocs ← Tactic.Doc.allTacticDocs (includeUnnamed := false)
   let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => {
@@ -643,7 +643,7 @@ def endSectionCompletion
     (id?               : Option Name)
     (danglingDot       : Bool)
     (scopeNames        : List String)
-    : IO (Array ResolvableCompletionItem) := do
+    : BaseIO (Array ResolvableCompletionItem) := do
   let mut idComponents := id?.map (fun id => id.components.toArray.map (·.toString)) |>.getD #[]
   if danglingDot then
     idComponents := idComponents.push ""
diff --git a/src/Lean/Server/Completion/CompletionResolution.lean b/src/Lean/Server/Completion/CompletionResolution.lean
index 04793ff57f14..fe1474762252 100644
--- a/src/Lean/Server/Completion/CompletionResolution.lean
+++ b/src/Lean/Server/Completion/CompletionResolution.lean
@@ -95,7 +95,7 @@ def resolveCompletionItem?
     (item              : CompletionItem)
     (id                : CompletionIdentifier)
     (completionInfoPos : Nat)
-    : IO CompletionItem := do
+    : EIO Exception CompletionItem := do
   let (completionInfos, _) := findCompletionInfosAt fileMap hoverPos cmdStx infoTree
   let some i := completionInfos[completionInfoPos]?
     | return item
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index a51b43e1894f..4acce81712be 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -130,15 +130,15 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
       let filter ctx info _ results := do
         let .ofTermInfo ti := info
           | return results
-        ctx.runMetaM info.lctx do
+        ctx.runMetaM info.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
           results.filterM fun (_, r) => do
             let .ofTermInfo childTi := r.info
               | return true
             return ! (← isInstanceProjectionInfoFor kind ti childTi)
-      let some info ← snap.infoTree.hoverableInfoAtM? (m := IO) hoverPos
+      let some info ← snap.infoTree.hoverableInfoAtM? (m := RequestM) hoverPos
           (includeStop := true) (filter := filter)
         | return #[]
-      locationLinksOfInfo doc.meta kind info snap.infoTree
+      locationLinksOfInfo doc.meta kind info snap.infoTree (← (← read).cancelTk.cancelTk)
 
 open Language in
 def findGoalsAt? (doc : EditableDocument) (hoverPos : String.Pos.Raw) : ServerTask (Option (List Elab.GoalsAtResult)) :=
@@ -193,13 +193,13 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
       let ciAfter := { ci with mctx := ti.mctxAfter }
       let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
       -- compute the interactive goals
-      let goals ← ci.runMetaM {} (do
+      let goals ← ci.runMetaM {} (cancelTk? := ← (← read).cancelTk.cancelTk) (do
         let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
         let goals ← goals.mapM Widget.goalToInteractive
         return ⟨goals⟩
       )
       -- compute the goal diff
-      ciAfter.runMetaM {} (do
+      ciAfter.runMetaM {} (cancelTk? := ← (← read).cancelTk.cancelTk) (do
           try
             Widget.diffInteractiveGoals useAfter ti goals
           catch _ =>
@@ -231,11 +231,11 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   mapTaskCostly (findInfoTreeAtPos doc hoverPos (includeStop := true)) <| Option.bindM fun infoTree => do
     let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := infoTree.termGoalAt? hoverPos
       | return none
-    let ty ← ci.runMetaM i.lctx do
+    let ty ← ci.runMetaM i.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
       instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
     -- for binders, hide the last hypothesis (the binder itself)
     let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-    let goal ← ci.runMetaM lctx' do
+    let goal ← ci.runMetaM lctx' (cancelTk? := ← (← read).cancelTk.cancelTk) do
       Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
     let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
     return some { goal with range, term := ← WithRpcRef.mk ti }
diff --git a/src/Lean/Server/FileWorker/SignatureHelp.lean b/src/Lean/Server/FileWorker/SignatureHelp.lean
index 9fac5c6ba9eb..4635b2689aba 100644
--- a/src/Lean/Server/FileWorker/SignatureHelp.lean
+++ b/src/Lean/Server/FileWorker/SignatureHelp.lean
@@ -18,7 +18,7 @@ namespace Lean.Server.FileWorker.SignatureHelp
 open Lean
 
 def determineSignatureHelp (tree : Elab.InfoTree) (appStx : Syntax)
-    : IO (Option Lsp.SignatureHelp) := do
+    : EIO Exception (Option Lsp.SignatureHelp) := do
   let some (appCtx, .ofTermInfo appInfo) := tree.smallestInfo? fun
       | .ofTermInfo ti =>
         -- HACK: Use range of syntax to figure out corresponding `TermInfo`.
@@ -97,7 +97,8 @@ private def isPositionInLineComment (text : FileMap) (pos : String.Pos.Raw) : Bo
 
 open CandidateKind in
 def findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext) (cmdStx : Syntax)
-    (tree : Elab.InfoTree) (requestedPos : String.Pos.Raw) : IO (Option Lsp.SignatureHelp) := do
+    (tree : Elab.InfoTree) (requestedPos : String.Pos.Raw) :
+    EIO Exception (Option Lsp.SignatureHelp) := do
   -- HACK: Since comments are whitespace, the signature help can trigger on comments.
   -- This is especially annoying on end-of-line comments, as the signature help will trigger on
   -- every space in the comment.
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index ef080d6400a7..05a272bfad5e 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -52,7 +52,7 @@ was stored for a particular `SubexprInfo` tag in a `TaggedText` generated with `
 def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
   | i => RequestM.pureTask do
     let i := i.val
-    i.ctx.runMetaM i.info.lctx do
+    i.ctx.runMetaM i.info.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
       let type? ← match (← i.info.type?) with
         | some type => some <$> ppExprTagged type
         | none => pure none
@@ -132,7 +132,7 @@ builtin_initialize
     fun ⟨kind, i⟩ => RequestM.pureTask do
       let i := i.val
       let rc ← read
-      let ls ← locationLinksOfInfo rc.doc.meta kind i
+      let ls ← locationLinksOfInfo rc.doc.meta kind i (cancelTk? := ← (← read).cancelTk.cancelTk)
       let ls := ls.map (·.toLocationLink)
       if !ls.isEmpty then return ls
       -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
@@ -146,7 +146,7 @@ builtin_initialize
         originInfo? := none
         children := PersistentArray.empty
       }
-      GoToM.run ctx i.ctx ti.lctx do
+      GoToM.run ctx i.ctx ti.lctx (cancelTk? := ← (← read).cancelTk.cancelTk) do
         let ls ← locationLinksFromDecl nm
         return ls.map (·.toLocationLink)
 
@@ -403,7 +403,7 @@ private structure Highlighted where
 
 variable (query : String) in
 private partial def highlightMatchesAux (msg : InteractiveMessage) :
-    IO Highlighted := do
+    EIO Exception Highlighted := do
   match msg with
   | .tag (.trace indent cls msg collapsed children) a => do
     let a : HighlightedInteractiveMessage := .ofInteractiveMessage a
diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean
index e2b08ca2c08a..9ea1f0e33ef1 100644
--- a/src/Lean/Server/GoTo.lean
+++ b/src/Lean/Server/GoTo.lean
@@ -86,9 +86,10 @@ structure GoToContext where
 
 abbrev GoToM α := ReaderT GoToContext MetaM α
 
-def GoToM.run (ctx : GoToContext) (ci : ContextInfo) (lctx : LocalContext) (act : GoToM α) :
-    IO α :=
-  ci.runMetaM lctx <| ReaderT.run act ctx
+def GoToM.run (ctx : GoToContext) (ci : ContextInfo) (lctx : LocalContext) (act : GoToM α)
+    (cancelTk? : Option IO.CancelToken := none) :
+    EIO Exception α :=
+  ci.runMetaM lctx (ReaderT.run act ctx) cancelTk?
 
 def locationLinksFromDecl (declName : Name) : GoToM (Array LeanLocationLink) := do
   let ctx ← read
@@ -308,7 +309,8 @@ def locationLinksFromCommandInfo (i : CommandInfo) : GoToM (Array LeanLocationLi
   locationLinksFromImport i
 
 def locationLinksOfInfo (doc : DocumentMeta) (kind : GoToKind) (ictx : InfoWithCtx)
-    (infoTree? : Option InfoTree := none) : IO (Array LeanLocationLink) := do
+    (infoTree? : Option InfoTree := none) (cancelTk? : Option IO.CancelToken := none)
+    : EIO Exception (Array LeanLocationLink) := do
   let ctx : GoToContext := {
     doc
     kind
@@ -316,7 +318,7 @@ def locationLinksOfInfo (doc : DocumentMeta) (kind : GoToKind) (ictx : InfoWithC
     originInfo? := some ictx.info
     children := ictx.children
   }
-  GoToM.run ctx ictx.ctx ictx.info.lctx do
+  GoToM.run ctx ictx.ctx ictx.info.lctx (cancelTk? := cancelTk?) do
     let ll ←
       match ictx.info with
       | .ofTermInfo ti =>
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 4c6726ee74ad..4c5c8ffe89de 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -356,7 +356,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   return none
 
 /-- Construct a hover popup, if any, from an info node in a context.-/
-def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
+def Info.fmtHover? (ci : ContextInfo) (i : Info) : EIO Exception (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do
     let mut fmts := #[]
     let mut infos := ∅
diff --git a/src/Lean/Server/RequestCancellation.lean b/src/Lean/Server/RequestCancellation.lean
index 58a78229d0f2..abf9472ddcd9 100644
--- a/src/Lean/Server/RequestCancellation.lean
+++ b/src/Lean/Server/RequestCancellation.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Server.ServerTask
+public import Lean.Server.Utils
 public import Init.System.Promise
 public import Init.System.CancelToken
 
@@ -30,6 +31,9 @@ def new : BaseIO RequestCancellationToken := do
     editCancellationPromise    := ← IO.Promise.new
   }
 
+def cancelTk (tk : RequestCancellationToken) : BaseIO IO.CancelToken :=
+  tk.cancelledByCancelRequest.merge tk.cancelledByEdit
+
 def cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit := do
   tk.cancelledByCancelRequest.set
   tk.requestCancellationPromise.resolve ()
@@ -63,14 +67,14 @@ structure RequestCancellation where
 def RequestCancellation.requestCancelled : RequestCancellation := {}
 
 abbrev CancellableT m := ReaderT RequestCancellationToken (ExceptT RequestCancellation m)
-abbrev CancellableM := CancellableT IO
+abbrev CancellableM := CancellableT (EIO Exception)
 
 def CancellableT.run (tk : RequestCancellationToken) (x : CancellableT m α) :
     m (Except RequestCancellation α) :=
   x tk
 
 def CancellableM.run (tk : RequestCancellationToken) (x : CancellableM α) :
-    IO (Except RequestCancellation α) :=
+    EIO Exception (Except RequestCancellation α) :=
   CancellableT.run tk x
 
 def CancellableT.checkCancelled [Monad m] [MonadLiftT BaseIO m] : CancellableT m Unit := do
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index 0679a83ecd0b..ede60e30f0de 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -181,8 +181,11 @@ def requestCancelled : RequestError :=
 def rpcNeedsReconnect : RequestError :=
   { code := ErrorCode.rpcNeedsReconnect, message := "Outdated RPC session" }
 
-def ofException (e : Lean.Exception) : IO RequestError :=
-  return internalError (← e.toMessageData.toString)
+def ofException (e : Lean.Exception) : BaseIO RequestError :=
+  if e.isInterrupt then
+    return .requestCancelled
+  else
+    return internalError (← e.toMessageData.toString)
 
 def ofIoError (e : IO.Error) : RequestError :=
   internalError (toString e)
@@ -330,6 +333,7 @@ def waitFindSnapAux (notFoundX : RequestM α) (x : Snapshot → RequestM α)
   /- The elaboration task that we're waiting for may be aborted if the file contents change.
   In that case, we reply with the `fileChanged` error by default. Thanks to this, the server doesn't
   get bogged down in requests for an old state of the document. -/
+  -- TODO: Does this also swallow `interrupt` exceptions?
   | Except.error e => throw (RequestError.ofIoError e)
   | Except.ok none => notFoundX
   | Except.ok (some snap) => x snap
@@ -436,20 +440,20 @@ partial def findInfoTreeAtPos
 open Elab.Command in
 def runCommandElabM (snap : Snapshot) (c : RequestT CommandElabM α) : RequestM α := do
   let rc ← readThe RequestContext
-  match ← snap.runCommandElabM rc.doc.meta (c.run rc) with
+  match ← snap.runCommandElabM rc.doc.meta (c.run rc) (← rc.cancelTk.cancelTk) with
   | .ok v => return v
   | .error e => throw e
 
 def runCoreM (snap : Snapshot) (c : RequestT CoreM α) : RequestM α := do
   let rc ← readThe RequestContext
-  match ← snap.runCoreM rc.doc.meta (c.run rc) with
+  match ← snap.runCoreM rc.doc.meta (c.run rc) (← rc.cancelTk.cancelTk) with
   | .ok v => return v
   | .error e => throw e
 
 open Elab.Term in
 def runTermElabM (snap : Snapshot) (c : RequestT TermElabM α) : RequestM α := do
   let rc ← readThe RequestContext
-  match ← snap.runTermElabM rc.doc.meta (c.run rc) with
+  match ← snap.runTermElabM rc.doc.meta (c.run rc) (← rc.cancelTk.cancelTk) with
   | .ok v => return v
   | .error e => throw e
 
@@ -537,7 +541,7 @@ def registerLspRequestHandler (method : String)
 
   requestHandlers.modify fun rhs => rhs.insert method { fileSource, handle }
 
-def lookupLspRequestHandler (method : String) : IO (Option RequestHandler) :=
+def lookupLspRequestHandler (method : String) : BaseIO (Option RequestHandler) :=
   return (← requestHandlers.get).find? method
 
 /-- NB: This method may only be called in `initialize` blocks (user or builtin).
@@ -790,7 +794,7 @@ def handleLspRequest (method : String) (params : Json) : RequestM (RequestTask S
         s!"request '{method}' routed through watchdog but unknown in worker; are both using the same plugins?"
     | some rh => rh.handle params
 
-def routeLspRequest (method : String) (params : Json) : IO (Except RequestError DocumentUri) := do
+def routeLspRequest (method : String) (params : Json) : BaseIO (Except RequestError DocumentUri) := do
   if ← isStatefulLspRequestMethod method then
     match ← lookupStatefulLspRequestHandler method with
     | none => return Except.error <| RequestError.methodNotFound method
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index e3b0fe5a8b3c..421009ec532e 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -53,23 +53,26 @@ def isAtEnd (s : Snapshot) : Bool :=
 
 open Command in
 /-- Use the command state in the given snapshot to run a `CommandElabM`.-/
-def runCommandElabM (snap : Snapshot) (doc : DocumentMeta) (c : CommandElabM α) : EIO Exception α := do
+def runCommandElabM (snap : Snapshot) (doc : DocumentMeta) (c : CommandElabM α)
+    (cancelTk? : Option IO.CancelToken := none) : EIO Exception α :=
   let ctx : Command.Context := {
     cmdPos := snap.stx.getPos? |>.getD 0,
     fileName := doc.uri,
     fileMap := doc.text,
     snap? := none
-    cancelTk? := none
+    cancelTk?
   }
   c.run ctx |>.run' snap.cmdState
 
 /-- Run a `CoreM` computation using the data in the given snapshot.-/
-def runCoreM (snap : Snapshot) (doc : DocumentMeta) (c : CoreM α) : EIO Exception α :=
-  snap.runCommandElabM doc <| Command.liftCoreM c
+def runCoreM (snap : Snapshot) (doc : DocumentMeta) (c : CoreM α)
+    (cancelTk? : Option IO.CancelToken := none) : EIO Exception α :=
+  snap.runCommandElabM doc (Command.liftCoreM c) cancelTk?
 
 /-- Run a `TermElabM` computation using the data in the given snapshot.-/
-def runTermElabM (snap : Snapshot) (doc : DocumentMeta) (c : TermElabM α) : EIO Exception α :=
-  snap.runCommandElabM doc <| Command.liftTermElabM c
+def runTermElabM (snap : Snapshot) (doc : DocumentMeta) (c : TermElabM α)
+    (cancelTk? : Option IO.CancelToken := none) : EIO Exception α :=
+  snap.runCommandElabM doc (Command.liftTermElabM c) cancelTk?
 
 end Snapshot
 
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 84cdabe30c00..75ca3f9a487d 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -21,6 +21,14 @@ namespace IO
 def throwServerError (err : String) : IO α :=
   throw (userError err)
 
+/-- Merge two cancellation tokens.
+The resulting token gets set as soon as any of the parents does. -/
+def CancelToken.merge (tk₁ : CancelToken) (tk₂ : CancelToken) : BaseIO CancelToken := do
+  let tk ← CancelToken.new
+  tk₁.onSet tk.set
+  tk₂.onSet tk.set
+  return tk
+
 namespace FS.Stream
 
 /--
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 5fc9e0b22a31..28ea45ec510b 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -112,10 +112,10 @@ private inductive EmbedFmt
   | ignoreTags
   deriving Inhabited
 
-private abbrev MsgFmtM := StateT (Array EmbedFmt) IO
+private abbrev MsgFmtM := StateT (Array EmbedFmt) BaseIO
 
 open MessageData in
-private partial def msgToInteractiveAux (msgData : MessageData) : IO (Format × Array EmbedFmt) :=
+private partial def msgToInteractiveAux (msgData : MessageData) : BaseIO (Format × Array EmbedFmt) :=
   go { currNamespace := Name.anonymous, openDecls := [] } none msgData |>.run #[]
 where
   pushEmbed (e : EmbedFmt) : MsgFmtM Nat :=
@@ -181,7 +181,7 @@ where
   | ctx?,     ofLazy f _          => do
     let dyn ← f (ctx?.map (mkPPContext nCtx))
     let some msg := dyn.get? MessageData
-      | throw <| IO.userError "MessageData.ofLazy: expected MessageData in Dynamic"
+      | return "[Error: MessageData.ofLazy: expected MessageData in Dynamic]"
     go nCtx ctx? msg
 
   /-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/
@@ -194,11 +194,12 @@ where
           f!"{children.size - blockSize} more entries..." more
     else children
 
-partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) : IO InteractiveMessage := do
+partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) :
+    EIO Exception InteractiveMessage := do
   if !hasWidgets then
     return (TaggedText.prettyTagged (← msgData.format)).rewrite fun _ tt => .text tt.stripTags
   let (fmt, embeds) ← msgToInteractiveAux msgData
-  let rec fmtToTT (fmt : Format) (indent : Nat) : IO InteractiveMessage :=
+  let rec fmtToTT (fmt : Format) (indent : Nat) : EIO Exception InteractiveMessage :=
     (TaggedText.prettyTagged fmt indent).rewriteM fun (n, col) tt =>
       match embeds[n]! with
         | .code ctx infos => do
@@ -252,9 +253,9 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
     if m.data.hasTag (· == `Tactic.unsolvedGoals) then some #[.unsolvedGoals]
     else if m.data.hasTag (· == `goalsAccomplished) then some #[.goalsAccomplished]
     else none
-  let message := match (← msgToInteractive m.data hasWidgets |>.toBaseIO) with
-    | .ok msg => msg
-    | .error ex => TaggedText.text s!"[error when printing message: {ex.toString}]"
+  let message ← match (← msgToInteractive m.data hasWidgets |>.toBaseIO) with
+    | .ok msg => pure msg
+    | .error ex => pure <| TaggedText.text s!"[error when printing message: {← ex.toMessageData.toString}]"
   let code? := (errorNameOfKind? m.kind).map (.string ·.toString)
   pure { range, fullRange? := some fullRange, severity?, source?, message, tags?, leanTags?, isSilent?, code? }