From 96ccf192e8a5fe216bbc63c688a06b2032bd14f5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 20 Dec 2022 18:10:12 +0100
Subject: [PATCH] fix: parenthesize `by` `optParam` values

---
 src/Lean/Parser/Term.lean   | 11 +++++++++++
 tests/lean/run/Reparen.lean |  1 +
 2 files changed, 12 insertions(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 1385f91e89..439143cf65 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -216,6 +216,17 @@ def binderTactic  := leading_parser
   atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
 def binderDefault := leading_parser
   " := " >> termParser
+
+open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
+@[combinator_parenthesizer Lean.Parser.Term.binderDefault] def binderDefault.parenthesizer : Parenthesizer := do
+  let prec := match (← getCur) with
+    -- must parenthesize to distinguish from `binderTactic`
+    | `(binderDefault| := by $_) => maxPrec
+    | _                          => 0
+  visitArgs do
+    term.parenthesizer prec
+    visitToken
+
 def explicitBinder (requireType := false) := ppGroup $ leading_parser
   "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
 /--
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 8e62ffb0dd..1683203355 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -51,3 +51,4 @@ open Lean
 syntax:80 term " ^~ " term:80 : term
 syntax:70 term " *~ " term:71 : term
 #eval check $ Unhygienic.run `(((1 + 2) *~ 3) ^~ 4)
+#eval check $ Unhygienic.run `(opaque foo (a := (by exact 1)) : True)