diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 2c7293329f..44d67cba55 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -104,11 +104,11 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType open Lean Elab Command Term Meta in def registerRpcProcedure (method : Name) : CoreM Unit := do let env ← getEnv - let errMsg := "Failed to register RPC call handler for '{method}'" + let errMsg := m!"Failed to register RPC call handler for '{method}'" if (←builtinRpcProcedures.get).contains method then - throwError s!"{errMsg}: already registered (builtin)" + throwError m!"{errMsg}: already registered (builtin)" if userRpcProcedures.contains env method then - throwError s!"{errMsg}: already registered" + throwError m!"{errMsg}: already registered" let wrappedName := method ++ `_rpc_wrapped let procT := mkConst ``RpcProcedure let proc ← MetaM.run' <| TermElabM.run' <| withoutErrToSorry do