From 6f9b80d91ce12372cbf6a3df4eee743caa4705b9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 7 May 2021 09:41:37 +0200 Subject: [PATCH] fix: parenthesizer: avoid panic on partial syntax trees Fixes #446 --- src/Lean/PrettyPrinter/Parenthesizer.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index fb7615a4b6..3ce78c0363 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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