From 40bb034b515eea1e44c638156d7befeeb1d1308d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 1 Apr 2021 16:42:04 +0200
Subject: [PATCH] fix: use pp.raw options when falling back to raw parser

---
 src/Lean/Util/PPExt.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index c08c3251ef..e570241e99 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -69,14 +69,15 @@ def ppExpr (ctx : PPContext) (e : Expr) : IO Format := do
         pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format :=
+  let fmtRaw := fun () => stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
   if pp.raw.get ctx.opts then
-    return stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
+    return fmtRaw ()
   else
     try
       ppExt.getState ctx.env |>.ppTerm ctx stx
     catch ex =>
       if pp.rawOnError.get ctx.opts then
-        pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{stx}"
+        pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{fmtRaw ()}"
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"