diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index b384ec570a..ffcf1bdde2 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -70,7 +70,7 @@ pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts
 protected def addContext (ref : Syntax) (msg : MessageData) : CommandElabM (Syntax × MessageData) := do
 ctx ← read;
 let ref := getBetterRef ref ctx.macroStack;
-let msg := addMacroStack msg ctx.macroStack;
+msg ← addMacroStack msg ctx.macroStack;
 msg ← Command.addContext' msg;
 pure (ref, msg)
 
@@ -103,7 +103,7 @@ match ea with
 
 private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
 let ref := getBetterRef ref ctx.macroStack;
-mkMessageAux ctx ref (addMacroStack (toString err) ctx.macroStack) MessageSeverity.error
+mkMessageAux ctx ref (toString err) MessageSeverity.error
 
 @[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α :=
 liftM x
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index cf4bd42122..496a059823 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -94,8 +94,6 @@ structure Context :=
    That is, it is safe to transition `errToSorry` from `true` to `false`, but
    we must not set `errToSorry` to `true` when it is currently set to `false`. -/
 (errToSorry      : Bool            := true)
-/- If `macroStackAtErr == true`, we include it in error messages. -/
-(macroStackAtErr : Bool            := true)
 
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind
@@ -245,7 +243,7 @@ instance MonadError : MonadError TermElabM :=
   addContext := fun ref msg => do
     ctx ← read;
     let ref := getBetterRef ref ctx.macroStack;
-    let msg := if ctx.macroStackAtErr then addMacroStack msg ctx.macroStack else msg;
+    msg ← addMacroStack msg ctx.macroStack;
     msg ← addMessageDataContext msg;
     pure (ref, msg) }
 
@@ -509,7 +507,7 @@ match f? with
 | some f => liftMetaM $ Meta.throwAppTypeMismatch f e extraMsg
 
 @[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
-adaptReader (fun (ctx : Context) => { ctx with macroStackAtErr := false }) x
+adaptTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := setMacroStackOption ctx.options false }) x
 
 /- Try to synthesize metavariable using type class resolution.
    This method assumes the local context and local instances of `instMVar` coincide
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 3ddfae67b4..b01f849a9d 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -39,13 +39,21 @@ match ref.getPos with
   | some elem => elem.before
   | none      => ref
 
-def addMacroStack (msgData : MessageData) (macroStack : MacroStack) : MessageData :=
+def ppMacroStackDefault := false
+@[init] def ppMacroStackOption : IO Unit :=
+registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
+def getMacroStackOption (o : Options) : Bool:= o.get `pp.macroStack ppMacroStackDefault
+def setMacroStackOption (o : Options) (flag : Bool) : Options := o.setBool `pp.macroStack flag
+
+def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) : m MessageData := do
+options ← getOptions;
+if !getMacroStackOption options then pure msgData else
 match macroStack with
-| []             => msgData
+| []             => pure msgData
 | stack@(top::_) =>
   let topFmt  := top.after.prettyPrint;
   let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ topFmt);
-  stack.foldl
+  pure $ stack.foldl
     (fun (msgData : MessageData) (elem : MacroStackElem) =>
       let macroFmt := elem.before.prettyPrint;
       msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt))
diff --git a/src/Lean/Util/PPGoal.lean b/src/Lean/Util/PPGoal.lean
index 851347c142..b88bef5ca0 100644
--- a/src/Lean/Util/PPGoal.lean
+++ b/src/Lean/Util/PPGoal.lean
@@ -7,10 +7,10 @@ import Lean.Util.PPExt
 
 namespace Lean
 
-def showAuxDeclsDefault := false
-@[init] def showAuxDeclsOption : IO Unit :=
-registerOption `pp.showAuxDecls { defValue := showAuxDeclsDefault, group := "pp", descr := "show auxiliary declarations used to compile recursive functions" }
-def getShowAuxDecls (o : Options) : Bool:= o.get `pp.showAuxDecls showAuxDeclsDefault
+def ppAuxDeclsDefault := false
+@[init] def ppAuxDeclsOption : IO Unit :=
+registerOption `pp.auxDecls { defValue := ppAuxDeclsDefault, group := "pp", descr := "display auxiliary declarations used to compile recursive functions" }
+def getAuxDeclsOption (o : Options) : Bool:= o.get `pp.auxDecls ppAuxDeclsDefault
 
 def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
 let env  := ppCtx.env;
@@ -20,7 +20,7 @@ match mctx.findDecl? mvarId with
 | none          => pure "unknown goal"
 | some mvarDecl => do
   let indent       := 2; -- Use option
-  let showAuxDecls := getShowAuxDecls opts;
+  let ppAuxDecls   := getAuxDeclsOption opts;
   let lctx         := mvarDecl.lctx;
   let lctx         := lctx.sanitizeNames opts;
   let ppCtx        := { ppCtx with lctx := lctx };
@@ -41,7 +41,7 @@ match mctx.findDecl? mvarId with
       };
   (varNames, type?, fmt) ← lctx.foldlM
     (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
-       if !showAuxDecls && localDecl.isAuxDecl then pure acc else
+       if !ppAuxDecls && localDecl.isAuxDecl then pure acc else
        let (varNames, prevType?, fmt) := acc;
        match localDecl with
        | LocalDecl.cdecl _ _ varName type _   =>
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index f2a0ccabe0..3409fb6cc9 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -27,10 +27,6 @@
 "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")"
 "#[]"
 StxQuot.lean:40:90: error: unexpected antiquotation splice
-with resulting expansion
-  run do a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns*) => pure eqns | _ => pure #[] 
-while expanding
-  run $ do a ← `(match a with | a => 1 | _ => 2); match_syntax a with `(match $e with $eqns*) => pure eqns | _ => pure #[] 
 StxQuot.lean:40:6: error: failed to create type class instance for 
   HasToString ?m
 StxQuot.lean:40:6: error: don't know how to synthesize placeholder
diff --git a/tests/lean/auxDeclIssue.lean b/tests/lean/auxDeclIssue.lean
index fc08c9f6c6..63a08d00b9 100644
--- a/tests/lean/auxDeclIssue.lean
+++ b/tests/lean/auxDeclIssue.lean
@@ -12,7 +12,7 @@ by {
   exact rfl
 }
 
-set_option pp.showAuxDecls true in
+set_option pp.auxDecls true in
 theorem ex1 : False :=
 by {
    assumption -- should not use the auxiliary declaration `ex1 : False`
diff --git a/tests/lean/letrec1.lean.expected.out b/tests/lean/letrec1.lean.expected.out
index 85d3bd670e..096b5f6bde 100644
--- a/tests/lean/letrec1.lean.expected.out
+++ b/tests/lean/letrec1.lean.expected.out
@@ -1,10 +1,4 @@
 letrec1.lean:6:0: error: 'f1.g' has already been declared
 letrec1.lean:18:35: error: unknown identifier 'g'
-with resulting expansion
-  HasLess.Less._@._internal._hyg.0 y g x 
-while expanding
-  y < g x 
-while expanding
-  { y : Nat // y < g x } 
 letrec1.lean:27:8: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously
 letrec1.lean:37:10: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously
diff --git a/tests/lean/macroStack.lean b/tests/lean/macroStack.lean
new file mode 100644
index 0000000000..1cdaccc796
--- /dev/null
+++ b/tests/lean/macroStack.lean
@@ -0,0 +1,8 @@
+new_frontend
+
+def f1 :=
+if h:x then 1 else 0
+
+set_option pp.macroStack true
+def f2 :=
+if h:(x > 0) then 1 else 0
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
new file mode 100644
index 0000000000..12e6a234b8
--- /dev/null
+++ b/tests/lean/macroStack.lean.expected.out
@@ -0,0 +1,8 @@
+macroStack.lean:4:5: error: unknown identifier 'x'
+macroStack.lean:8:6: error: unknown identifier 'x'
+with resulting expansion
+  Greater._@._internal._hyg.0 x 0 
+while expanding
+  x > 0 
+while expanding
+  if h:(x > 0) then 1 else 0 
diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out
index 46dc3ed0c3..2d45ecaec6 100644
--- a/tests/lean/protected.lean.expected.out
+++ b/tests/lean/protected.lean.expected.out
@@ -7,23 +7,8 @@ protected.lean:22:7: error: unknown identifier 'y'
 Bla.Foo.z : Nat
 protected.lean:25:14: error: protected declarations must be in a namespace
 protected.lean:28:14: error: unknown identifier 'f'
-with resulting expansion
-  HasMul.mul._@._internal._hyg.0 f (x-1) 2 
-while expanding
-  f (x-1) * 2 
-while expanding
-  if x > 0 then f (x-1) * 2 else 1 
-while expanding
-  protected partial def Foo.f (x : Nat) :=
-  if x > 0 then f (x-1) * 2 else 1 
 8
 protected.lean:38:14: error: unknown identifier 'g'
-with resulting expansion
-  HasMul.mul._@._internal._hyg.0 g (x-1) 2 
-while expanding
-  g (x-1) * 2 
-while expanding
-  if x > 0 then g (x-1) * 2 else 1 
 protected.lean:47:6: error: unknown identifier 'g'
 protected.lean:47:0: error: application type mismatch
   Lean.runEval (sorryAx ?m)
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index d27b492079..6dad7df6d2 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -14,15 +14,6 @@ but it is expected to have type
   x=x
 failed to synthesize instance
   CoeT (x=x) _ (x=x)
-with resulting expansion
-   section set_option pp.sanitizeNames false theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
-  h -- this error is confusing because we have disabled `pp.sanitizeNames`
-  
-   end 
-while expanding
-  set_option pp.sanitizeNames false in
-  theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x :=
-  h 
 shadow.lean:13:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1