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

chore: fall back to raw printer on pretty printing failure

Browse source 
/cc @leodemoura
This commit is contained in:
Sebastian Ullrich 2020-11-28 11:10:17 +01:00
parent 2a5c85d9e3
commit b41301747d
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Util/PPExt.lean
View file

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