max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add docstring for chainLspRequestHandler

Browse source
This commit is contained in:
tydeu 2021-12-23 17:40:08 -05:00 • committed by Sebastian Ullrich
parent 004e172f5d
commit 30bdd4e751
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Server/Requests.lean
View file

@ -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]