diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index afac3a92e0..e0c1690c1f 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -327,6 +327,19 @@ structure Parser where
 
 abbrev TrailingParser := Parser
 
+def dbgTraceStateFn (label : String) (p : ParserFn) : ParserFn :=
+  fun c s =>
+    let sz := s.stxStack.size
+    let s' := p c s
+    dbg_trace "{label}
+  pos: {s'.pos}
+  err: {s'.errorMsg}
+  out: {s'.stxStack.extract sz s'.stxStack.size}" s'
+
+def dbgTraceState (label : String) (p : Parser) : Parser where
+  fn   := dbgTraceStateFn label p.fn
+  info := p.info
+
 @[noinline] def epsilonInfo : ParserInfo :=
   { firstTokens := FirstTokens.epsilon }
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 960a1a1305..b34f57a857 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -450,6 +450,8 @@ def interpolatedStr.formatter (p : Formatter) : Formatter := do
     | some str => push str *> goLeft
     | none     => p
 
+@[combinatorFormatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (label : String) (p : Formatter) : Formatter := p
+
 @[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
   if c then t else e
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 82342278a8..dc6d5df08d 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -494,6 +494,8 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do
     else
       p
 
+@[combinatorParenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (label : String) (p : Parenthesizer) : Parenthesizer := p
+
 @[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
   if c then t else e