fix: line break in simp? output (#6048)

This PR fixes `simp?` suggesting output with invalid indentation 

Fixes #6006

src/Init/Tactics.lean

@@ -466,7 +466,7 @@ hypotheses or the goal. It can have one of the forms:
 * `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
 * `at *`: target all hypotheses and the goal
 -/
-syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
+syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
 
 /--
 * `change tgt'` will change the goal from `tgt` to `tgt'`,

tests/lean/interactive/builtinCodeactions.lean

@@ -0,0 +1,7 @@
+/-- Must not introduce line break between `at` and `h` -/
+example {a b c d : Nat} (h : a = b)
+    (AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA : b = c)
+    (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : c = d) :
+    a = b := by
+  simp? [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h
+  --^ codeAction

tests/lean/interactive/builtinCodeactions.lean.expected.out

@@ -0,0 +1,13 @@
+{"title":
+ "Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h",
+ "kind": "quickfix",
+ "isPreferred": true,
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///builtinCodeactions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 5, "character": 2},
+       "end": {"line": 5, "character": 97}},
+      "newText":
+      "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}}