chore: add limited public API for builtinRpcProcedures (#10499)

This is not a complete public API, just enough to avoid an `open
private` in ProofWidgets.
This commit is contained in:
Kim Morrison 2025-09-22 21:20:25 +10:00 committed by GitHub
parent 85ce814689
commit a4dcb25f69
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

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