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

fix: parenthesizer: avoid panic on partial syntax trees

Browse source 
Fixes #446
This commit is contained in:
Sebastian Ullrich 2021-05-07 09:41:37 +02:00
parent 475f5fecaa
commit 6f9b80d91c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -207,7 +207,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
trace[PrettyPrinter.parenthesize] "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
x
let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
| panic! s!"maybeParenthesize: visited a syntax tree without precedences?!{line ++ fmt stx}"
| trace[PrettyPrinter.parenthesize] "visited a syntax tree without precedences?!{line ++ fmt stx}"
trace[PrettyPrinter.parenthesize] ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
-- Should we parenthesize?
if (prec > minPrec || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then