From 2348fb37d380bb11f9d5bfee5be5d6004eaed589 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 10 Jun 2023 15:10:40 -0400 Subject: [PATCH] fix: use `Lean.initializing` instead of `IO.initializing` --- src/Lean/Parser/Extension.lean | 2 +- src/Lean/Server/Rpc/RequestHandling.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 5165eb64c5..70fecd0ee6 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -177,7 +177,7 @@ inductive AliasValue (α : Type) where abbrev AliasTable (α) := NameMap (AliasValue α) def registerAliasCore {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do - unless (← IO.initializing) do throw ↑"aliases can only be registered during initialization" + unless (← initializing) do throw ↑"aliases can only be registered during initialization" if (← mapRef.get).contains aliasName then throw ↑s!"alias '{aliasName}' has already been declared" mapRef.modify (·.insert aliasName value) diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 75614e7e3c..2c7293329f 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -93,7 +93,7 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType [RpcEncodable paramType] [RpcEncodable respType] (handler : paramType → RequestM (RequestTask respType)) : IO Unit := do let errMsg := s!"Failed to register builtin RPC call handler for '{method}'" - unless (← IO.initializing) do + unless (← initializing) do throw <| IO.userError s!"{errMsg}: only possible during initialization" if (←builtinRpcProcedures.get).contains method then throw <| IO.userError s!"{errMsg}: already registered"