From a4dcb25f69e020bcd0328ff189cad5be40159edc Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 22 Sep 2025 21:20:25 +1000
Subject: [PATCH] chore: add limited public API for builtinRpcProcedures
 (#10499)

This is not a complete public API, just enough to avoid an `open
private` in ProofWidgets.
---
 src/Lean/Server/Rpc/RequestHandling.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 8664f6651c..fd08356b20 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -36,6 +36,10 @@ private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (
 private opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) :
     Except String RpcProcedure
 
+/-- Checks whether a builtin RPC procedure exists with the given name. -/
+def existsBuiltinRpcProcedure (method : Name) : IO Bool := do
+  return (← builtinRpcProcedures.get).contains method
+
 open RequestM in
 def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
   -- The imports are finished at this point, because the handleRequest function