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

fix: uninterpolated error message in registerRpcProcedure (#2547)

Browse source
This commit is contained in:
thorimur 2023-09-18 05:39:04 -04:00 • committed by GitHub
parent c4bd112a7f
commit 018020d36f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Server/Rpc/RequestHandling.lean
View file

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