From 3bdb98e5ee280b6e3f94a80ec7df8bf984e63e12 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Tue, 17 May 2022 18:26:27 -0400 Subject: [PATCH] feat: rpc attribute Functions can now be marked with the `@[rpc]` attribute, which registers the function as an RpcProcedure that can be used to communicate with the code editor and infoview. --- src/Lean/Server/Rpc/RequestHandling.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 19820c843d..197b70d8cc 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -121,4 +121,15 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do } setEnv <| userRpcProcedures.insert (← getEnv) method wrappedName +builtin_initialize registerBuiltinAttribute { + name := `rpc + descr := "Marks a function as a Lean server RPC method. + Shorthand for `registerRpcProcedure`. + The function must have type `α → RequestM (RequestTask β)` with + RpcEncodings for both α and β." + applicationTime := AttributeApplicationTime.afterCompilation + add := fun decl stx kind => + registerRpcProcedure decl +} + end Lean.Server