From b41301747d0dc738e5362014008df857e6fc8b37 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 28 Nov 2020 11:10:17 +0100
Subject: [PATCH] chore: fall back to raw printer on pretty printing failure

/cc @leodemoura
---
 src/Lean/Util/PPExt.lean | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index d74e3ae7c2..8c10ae3a65 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -44,18 +44,24 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
 builtin_initialize ppExt : EnvExtension PPFns ←
   registerEnvExtension ppFnsRef.get
 
-def ppExpr (ctx : PPContext) (e : Expr) : IO Format :=
+def ppExpr (ctx : PPContext) (e : Expr) : IO Format := do
   let e := ctx.mctx.instantiateMVars e |>.1
   if getPPRaw ctx.opts then
     return format (toString e)
   else
-    ppExt.getState ctx.env |>.ppExpr ctx e
+    try
+      ppExt.getState ctx.env |>.ppExpr ctx e
+    catch ex =>
+      pure f!"[Error pretty printing expression: {ex}. Falling back to raw printer.]{Format.line}{e}"
 
 def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format :=
   if getPPRaw ctx.opts then
     return stx.formatStx (getSyntaxMaxDepth ctx.opts)
   else
-    ppExt.getState ctx.env |>.ppTerm ctx stx
+    try
+      ppExt.getState ctx.env |>.ppTerm ctx stx
+    catch ex =>
+      pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{stx}"
 
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
     ppExt.getState ctx.env |>.ppGoal ctx mvarId