From f3976fc53a883ac7606fc59357d43f4b51016ca7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 May 2020 14:43:15 +0200 Subject: [PATCH] chore: parenthesizer: address some comments --- src/Init/Lean/PrettyPrinter/Parenthesizer.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean index b899b4df89..f827d3812f 100644 --- a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean @@ -30,12 +30,12 @@ produced by `p rbp` if Note that in case 2, it is also sufficient to parenthesize a *parent* node as long as the offending token is still to the right of that node. For example, imagine the tree structure of `(f $ fun x => x) y` without parentheses. We need to -insert *some* parentheses between `x` and `y` since the lambda body is parse with precedence 0, while `y` as an +insert *some* parentheses between `x` and `y` since the lambda body is parsed with precedence 0, while `y` as an identifier has precedence `appPrec`. But we need to parenthesize the `$` node anyway since the precedence of its RHS (0) again is smaller than that of `y`. So it's better to only parenthesize the outer node than ending up with `(f $ (fun x => x)) y`. -Unfortunately, we cannot determine the precedence of a token just by looking at the syntax tree because it can actually +Unfortunately, we cannot determine the precedence of a token just by looking at the token table because it can actually have different precedences in different contexts (e.g. because of whitespace sensitivity). Thus we need to look at the parser that produced the token as well.