From 4d428c86600866b01cbbbe25d39dd96a16815b4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2020 06:54:03 -0800
Subject: [PATCH] feat: add `ScopedEnvExtension.addLocalEntry`

---
 src/Lean/Parser/Extension.lean   | 4 ++--
 src/Lean/ScopedEnvExtension.lean | 8 ++++++++
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 51540753bd..1535814c70 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -495,8 +495,8 @@ private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : N
   match addParser categories catName declName leading parser prio, kind with
   | Except.error ex, _ => throwError ex
   | Except.ok _, AttributeKind.global => modifyEnv fun env => parserExtension.addEntry env entry
-  | Except.ok _, AttributeKind.scoped => modifyEnv fun env  => parserExtension.addScopedEntry env (← getCurrNamespace) entry
-  | Except.ok _, AttributeKind.local  => throwError! "local parsers have not been implemented yet"
+  | Except.ok _, AttributeKind.scoped => modifyEnv fun env => parserExtension.addScopedEntry env (← getCurrNamespace) entry
+  | Except.ok _, AttributeKind.local  => modifyEnv fun env => parserExtension.addLocalEntry env entry
   runParserAttributeHooks catName declName (builtin := false)
 
 def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl where
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index 3f7dcd553f..7783803b6b 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -142,6 +142,14 @@ def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Envir
 def ScopedEnvExtension.addScopedEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) (b : β) : Environment :=
   ext.ext.addEntry env (Entry.«scoped» namespaceName b)
 
+def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
+  let s := ext.ext.getState env
+  match s.stateStack with
+  | [] => env
+  | top :: states =>
+    let top := { top with state := ext.descr.addEntry top.state b }
+    ext.ext.setState env { s with stateStack := top :: states }
+
 def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
   match ext.ext.getState env |>.stateStack with
   | top :: _ => top.state