max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: prevent infinite recursion on pretty printer failure

Browse source
This commit is contained in:
Sebastian Ullrich 2020-09-15 18:41:37 +02:00 • committed by Leonardo de Moura
parent b54fe2e17a
commit 01ac1b1fda
1 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/PrettyPrinter.lean
View file

@ -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