diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 70f7f6120d..3199d4af04 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -40,7 +40,7 @@ instance : ToJson String := ⟨fun s => s⟩
 instance [FromJson α] : FromJson (Array α) where
   fromJson?
     | Json.arr a => a.mapM fromJson?
-    | _          => throw "JSON array expected"
+    | j          => throw s!"expected JSON array, got '{j}'"
 
 instance [ToJson α] : ToJson (Array α) :=
   ⟨fun a => Json.arr (a.map toJson)⟩
@@ -55,6 +55,17 @@ instance [ToJson α] : ToJson (Option α) :=
     | none   => Json.null
     | some a => toJson a⟩
 
+instance [FromJson α] [FromJson β] : FromJson (α × β) where
+  fromJson?
+    | Json.arr #[ja, jb] => do
+      let a ← fromJson? ja
+      let b ← fromJson? jb
+      return (a, b)
+    | j => throw s!"expected pair, got '{j}'"
+
+instance [ToJson α] [ToJson β] : ToJson (α × β) where
+  toJson := fun (a, b) => Json.arr #[toJson a, toJson b]
+
 instance : FromJson Name where
   fromJson? j := do
     let s ← j.getStr?
@@ -101,7 +112,7 @@ namespace Json
 instance : FromJson Structured := ⟨fun
   | arr a => Structured.arr a
   | obj o => Structured.obj o
-  | _     => throw "structured object expected"⟩
+  | j     => throw s!"expected structured object, got '{j}'"⟩
 
 instance : ToJson Structured := ⟨fun
   | Structured.arr a => arr a
diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean
index 558b9ddcf4..fe6627b1a5 100644
--- a/src/Lean/Server/FileWorker/Utils.lean
+++ b/src/Lean/Server/FileWorker/Utils.lean
@@ -84,7 +84,8 @@ end RpcSessionState
 structure RpcSession where
   sessionId       : UInt64
   clientConnected : Bool
-  -- A single `Ref` ensures atomic transactions.
+  /-- We allow asynchronous elab tasks and request handlers to modify the state.
+  A single `Ref` ensures atomic transactions. -/
   state           : IO.Ref RpcSessionState
 
 namespace RpcSession
diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 9254288f16..e4201d093f 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -82,6 +82,7 @@ structure RpcEncoding.DerivingParams where
 /-- Marks fields to encode as opaque references in LSP packets. -/
 structure WithRpcRef (α : Type u) where
   val : α
+  deriving Inhabited
 
 namespace WithRpcRef