From 4878f0d13e2518d9ea3b21c592e45eaec21743ac Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 25 Dec 2020 16:10:23 +0100
Subject: [PATCH] fix: delaborator: correctly toggle individual when setting
 `pp.all`

---
 src/Lean/PrettyPrinter/Delaborator/Basic.lean | 23 +++++++++----------
 tests/lean/236.lean                           | 11 +++++++++
 tests/lean/236.lean.expected.out              |  3 +++
 3 files changed, 25 insertions(+), 12 deletions(-)
 create mode 100644 tests/lean/236.lean
 create mode 100644 tests/lean/236.lean.expected.out

diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index decdf33574..6587c17080 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -33,18 +33,18 @@ import Lean.Elab.Term
 
 namespace Lean
 
-def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
-def getPPCoercions (o : Options) : Bool := o.get `pp.coercions true
-def getPPExplicit (o : Options) : Bool := o.get `pp.explicit false
-def getPPNotation (o : Options) : Bool := o.get `pp.notation true
-def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections true
-def getPPStructureInstances (o : Options) : Bool := o.get `pp.structure_instances true
-def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_instance_type false
-def getPPUniverses (o : Options) : Bool := o.get `pp.universes false
-def getPPFullNames (o : Options) : Bool := o.get `pp.full_names false
-def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names false
-def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
 def getPPAll (o : Options) : Bool := o.get `pp.all false
+def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types (!getPPAll o)
+def getPPCoercions (o : Options) : Bool := o.get `pp.coercions (!getPPAll o)
+def getPPExplicit (o : Options) : Bool := o.get `pp.explicit (getPPAll o)
+def getPPNotation (o : Options) : Bool := o.get `pp.notation (!getPPAll o)
+def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections (!getPPAll o)
+def getPPStructureInstances (o : Options) : Bool := o.get `pp.structure_instances (!getPPAll o)
+def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_instance_type (getPPAll o)
+def getPPUniverses (o : Options) : Bool := o.get `pp.universes (getPPAll o)
+def getPPFullNames (o : Options) : Bool := o.get `pp.full_names (getPPAll o)
+def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names (getPPAll o)
+def getPPUnicode (o : Options) : Bool := o.get `pp.unicode (!getPPAll o)
 
 builtin_initialize
   registerOption `pp.explicit { defValue := false, group := "pp", descr := "(pretty printer) display implicit arguments" }
@@ -143,7 +143,6 @@ def getExprKind : DelabM Name := do
 /-- Evaluate option accessor, using subterm-specific options if set. Default to `true` if `pp.all` is set. -/
 def getPPOption (opt : Options → Bool) : DelabM Bool := do
   let ctx ← read
-  let opt := fun opts => opt opts || getPPAll opts
   let val := opt ctx.defaultOptions
   match ctx.optionsPerPos.find? ctx.pos with
   | some opts => pure $ opt opts
diff --git a/tests/lean/236.lean b/tests/lean/236.lean
new file mode 100644
index 0000000000..6f6dc59f10
--- /dev/null
+++ b/tests/lean/236.lean
@@ -0,0 +1,11 @@
+structure Foo where
+  x : Nat
+  b : Bool
+
+#check { x := 10, b := true : Foo }
+
+set_option pp.all true
+#check { x := 10, b := true : Foo }
+
+set_option pp.structure_instances true
+#check { x := 10, b := true : Foo }
diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out
new file mode 100644
index 0000000000..7f1b8c1794
--- /dev/null
+++ b/tests/lean/236.lean.expected.out
@@ -0,0 +1,3 @@
+{ x := 10, b := true } : Foo
+Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
+{ x := @OfNat.ofNat.{0} Nat 10 (instOfNatNat 10), b := Bool.true : Foo } : Foo