def
Lean.Server.registerRpcCallHandler
(method : Lean.Name)
(paramType : Type)
(respType : Type)
{paramLspType : outParam Type}
[inst : Lean.Server.RpcEncoding paramType paramLspType]
[inst : Lean.FromJson paramLspType]
{respLspType : outParam Type}
[inst : Lean.Server.RpcEncoding respType respLspType]
[inst : Lean.ToJson respLspType]
(handler : paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType))
:
Equations
- Lean.Server.registerRpcCallHandler method paramType respType handler = do let a ← liftM IO.initializing let _do_jp : PUnit → IO Unit := fun y => do let a ← ST.Ref.get Lean.Server.rpcProcedures let _do_jp : PUnit → IO Unit := fun y => let wrapper := fun seshId j => do let rc ← read let discr ← pure (Std.RBMap.find? rc.rpcSessions seshId) match discr with | some seshRef => do let t ← Lean.Server.RequestM.asTask do let paramsLsp ← liftExcept (Lean.Server.parseRequestParams paramLspType j) let act : ExceptT String (StateM Lean.Server.FileWorker.RpcSession) paramType := Lean.Server.rpcDecode paramsLsp let a ← ST.Ref.get seshRef match StateT.run' act a with | Except.ok v => pure v | Except.error e => throwThe Lean.Server.RequestError { code := Lean.JsonRpc.ErrorCode.invalidParams, message := toString "Cannot decode params in RPC call '" ++ toString method ++ toString "(" ++ toString (Lean.Json.compress j) ++ toString ")'\n" ++ toString e ++ toString "" } let t ← Lean.Server.RequestM.bindTask t fun x => match x with | Except.error e => throw e | Except.ok ps => handler ps Lean.Server.RequestM.mapTask t fun x => match x with | Except.error e => throw e | Except.ok ret => let act := Lean.Server.rpcEncode ret; do let a ← ST.Ref.modifyGet seshRef (StateT.run act) pure (Lean.toJson a) | x => throwThe Lean.Server.RequestError { code := Lean.JsonRpc.ErrorCode.rpcNeedsReconnect, message := toString "Outdated RPC session" }; ST.Ref.modify Lean.Server.rpcProcedures fun ps => Std.PersistentHashMap.insert ps method { wrapper := wrapper } if Std.PersistentHashMap.contains a method = true then do let y ← throw (IO.userError (toString "Failed to register RPC call handler for '" ++ toString method ++ toString "': already registered")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if (!a) = true then do let y ← throw (IO.userError (toString "Failed to register RPC call handler for '" ++ toString method ++ toString "': only possible during initialization")) _do_jp y else do let y ← pure PUnit.unit _do_jp y