From 30bdd4e7516f37efcf29be1a0f336adc9bd26eb9 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 23 Dec 2021 17:40:08 -0500
Subject: [PATCH] doc: add docstring for `chainLspRequestHandler`

---
 src/Lean/Server/Requests.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index ddfc4d3052..b1a8fce92c 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -153,6 +153,13 @@ def registerLspRequestHandler (method : String)
 def lookupLspRequestHandler (method : String) : IO (Option RequestHandler) := do
   (← requestHandlers.get).find? method
 
+/-- NB: This method may only be called in `builtin_initialize` blocks.
+
+Register another handler to invoke after the last one registered for a method.
+At least one handler for the method must have already been registered to perform
+chaining.
+
+For more details on the registration of a handler, see `registerLspRequestHandler`. -/
 def chainLspRequestHandler (method : String)
     paramType [FromJson paramType]
     respType [FromJson respType] [ToJson respType]