From 01ac1b1fdac34a70454f8709fcb847c48f894f90 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Sep 2020 18:41:37 +0200
Subject: [PATCH] fix: prevent infinite recursion on pretty printer failure

---
 src/Lean/PrettyPrinter.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index a5b8da67c6..cedbeec914 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -24,8 +24,17 @@ parenthesizeCommand stx >>= formatCommand
 def ppModule (stx : Syntax) : CoreM Format := do
 parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
 
+private partial def noContext : MessageData → MessageData
+| MessageData.withContext ctx msg => noContext msg
+| msg => msg
+
 def ppExprFn (ppCtx : PPContext) (e : Expr) : IO Format := do
-(fmt, _, _) ← (ppExpr e).toIO { options := ppCtx.opts } { env := ppCtx.env } { lctx := ppCtx.lctx } { mctx := ppCtx.mctx };
+let pp : MetaM Format := adaptExcept (fun ex => match ex with
+  -- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
+  | Exception.error ref msg => Exception.error ref (noContext msg)
+  | e                       => e)
+  (ppExpr e);
+(fmt, _, _) ← pp.toIO { options := ppCtx.opts } { env := ppCtx.env } { lctx := ppCtx.lctx } { mctx := ppCtx.mctx };
 pure fmt
 
 -- TODO: activate when ready