From 0838b95105e5b5ea4a573adff47ad7937fbd20b4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Apr 2021 16:11:12 -0700
Subject: [PATCH] chore: add `Macro.State.Extra`

---
 src/Init/Prelude.lean   | 7 +++++++
 src/Lean/Elab/Util.lean | 3 ++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 482a465a12..a7df90b09e 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2042,8 +2042,15 @@ inductive Exception where
   | error             : Syntax → String → Exception
   | unsupportedSyntax : Exception
 
+constant State.ExtraPointed : PointedType.{0}
+
+def State.Extra : Type := State.ExtraPointed.type
+instance : Inhabited State.Extra where
+  default := State.ExtraPointed.val
+
 structure State where
   macroScope : MacroScope
+  extra      : State.Extra
   deriving Inhabited
 
 end Macro
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 49c03988a8..fae2cf8a63 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -161,7 +161,8 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
             mainModule     := env.mainModule,
             currRecDepth   := ← MonadRecDepth.getRecDepth,
-            maxRecDepth    := ← MonadRecDepth.getMaxRecDepth } { macroScope := (← MonadMacroAdapter.getNextMacroScope) } with
+            maxRecDepth    := ← MonadRecDepth.getMaxRecDepth }
+          { macroScope := (← MonadMacroAdapter.getNextMacroScope), extra := arbitrary } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
   | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg
   | EStateM.Result.ok a  s                                   => MonadMacroAdapter.setNextMacroScope s.macroScope; pure a