diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 0c3afd28e4..059ca84ae0 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -68,6 +68,8 @@ builtin_initialize
     FileWorker.getInteractiveTermGoal
 
 structure GetInteractiveDiagnosticsParams where
+  /-- Return diagnostics for these lines only if present,
+  otherwise return all diagnostics. -/
   lineRange? : Option Lsp.LineRange
   deriving Inhabited, FromJson, ToJson
 
@@ -76,12 +78,15 @@ def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : Reque
   let doc ← readDoc
   let rangeEnd ← params.lineRange?.map fun range =>
     doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
-  withWaitFindSnap doc (fun snap => rangeEnd.all (· ≤ snap.endPos)) #[]
-    fun snap => snap.interactiveDiags.toArray.filter fun diag =>
-      params.lineRange?.all fun ⟨s, e⟩ =>
-        -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
-        s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
-        diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
+  let t ← doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
+  t.map fun (snaps, _) =>
+    let diags? := snaps.getLast?.map fun snap =>
+      snap.interactiveDiags.toArray.filter fun diag =>
+        params.lineRange?.all fun ⟨s, e⟩ =>
+          -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
+          s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
+          diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
+    diags?.getD #[]
 
 builtin_initialize
   registerRpcCallHandler
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index bead5e42a3..f95deaf452 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -95,9 +95,9 @@ def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (Re
     | Except.error e => throwThe RequestError e
     | Except.ok v    => v
 
-/-- Create a task which waits for a snapshot matching `p`, handles various errors,
-and if a matching snapshot was found executes `x` with it. If not found, the task
-executes `notFoundX`. -/
+/-- Create a task which waits for the first snapshot matching `p`, handles various errors,
+and if a matching snapshot was found executes `x` with it. If not found, the task executes
+`notFoundX`. -/
 def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
   (notFoundX : RequestM β)
   (x : Snapshot → RequestM β)
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index d5d31cd2c8..b7dcd15660 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -78,6 +78,7 @@ private def formatWithOpts (e : Expr) (optsPerPos : Delaborator.OptionsPerPos)
     let currNamespace ← getCurrNamespace
     let openDecls ← getOpenDecls
     let opts ← getOptions
+    let e ← Meta.instantiateMVars e
     let (stx, infos) ← PrettyPrinter.delabCore currNamespace openDecls e optsPerPos
     let stx := sanitizeSyntax stx |>.run' { options := opts }
     let stx ← PrettyPrinter.parenthesizeTerm stx