fix: only print named patterns inside patterns

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -671,6 +671,7 @@ where
 
 @[builtinDelab app.namedPattern]
 def delabNamedPattern : Delab := do
+  guard (← read).inPattern
   guard $ (← getExpr).getAppNumArgs == 3
   let x ← withAppFn $ withAppArg delab
   let p ← withAppArg delab

tests/lean/run/PPTopDownAnalyze.lean

@@ -227,6 +227,7 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 #testDelabN MonadLift.noConfusionType
 #testDelabN MonadExcept.noConfusion
 #testDelabN MonadFinally.noConfusion
+#testDelabN Lean.Elab.InfoTree.goalsAt?.match_1
 
 -- TODO: this test is broken because of the inability to solve structural max constraints
 -- (See https://github.com/leanprover/lean4/issues/590)
@@ -237,6 +238,3 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 -- TODO: this is broken because it is currently inaccessible names
 -- #testDelabN Std.ShareCommon.ObjectMap.find?
 -- #testDelabN Std.ShareCommon.ObjectMap.insert
-
--- TODO: these fail because we are not disable named patterns when not using `match` syntax
--- #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1