diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 0097b62e02..97f7886f93 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -175,6 +175,7 @@ def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
 @[combinatorFormatter Lean.Parser.categoryParser]
 def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
   let stx ← getCur
+  trace[PrettyPrinter.format]! "formatting {MessageData.nest 2 (Format.line ++ fmt stx)}"
   if stx.getKind == `choice then
     visitArgs do
       let stx ← getCur;
@@ -266,7 +267,7 @@ def symbol.formatter (sym : String) : Formatter := do
     pushToken sym;
     goLeft
   else do
-    trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{stx}', expected symbol '{sym}'"
+    trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
     throwBacktrack
 
 @[combinatorFormatter Lean.Parser.nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
@@ -453,13 +454,14 @@ end Formatter
 open Formatter
 
 def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
-let options ← getOptions
-let table ← Parser.builtinTokenTable.get
-catchInternalId backtrackExceptionId
-  (do
-    let (_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
-    pure $ Format.fill $ st.stack.get! 0)
-  (fun _ => throwError "format: uncaught backtrack exception")
+  trace[PrettyPrinter.format.input]! "{fmt stx}"
+  let options ← getOptions
+  let table ← Parser.builtinTokenTable.get
+  catchInternalId backtrackExceptionId
+    (do
+      let (_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
+      pure $ Format.fill $ st.stack.get! 0)
+    (fun _ => throwError "format: uncaught backtrack exception")
 
 def formatTerm := format $ categoryParser.formatter `term
 def formatCommand := format $ categoryParser.formatter `command
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 328c3a67a6..e59b420799 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -208,7 +208,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
   let st ← get
   -- reset precs for the recursive call
   set { stxTrav := st.stxTrav : State }
-  trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ stx)}"
+  trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ fmt stx)}"
   x
   let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
     | panic! "maybeParenthesize: visited a syntax tree without precedences?!"
@@ -532,7 +532,8 @@ end Parenthesizer
 open Parenthesizer
 
 /-- Add necessary parentheses in `stx` parsed by `parser`. -/
-def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :=
+def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
+  trace[PrettyPrinter.parenthesize.input]! "{fmt stx}"
   catchInternalId backtrackExceptionId
     (do
       let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }