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

fix: use pp.raw options when falling back to raw parser

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-01 16:42:04 +02:00
parent 2837873db5
commit 40bb034b51
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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