diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 78c9959b33..a5631e9b18 100644 --- a/src/Init/Tactics.lean +++ b/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'`, diff --git a/tests/lean/interactive/builtinCodeactions.lean b/tests/lean/interactive/builtinCodeactions.lean new file mode 100644 index 0000000000..3c829d241f --- /dev/null +++ b/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 diff --git a/tests/lean/interactive/builtinCodeactions.lean.expected.out b/tests/lean/interactive/builtinCodeactions.lean.expected.out new file mode 100644 index 0000000000..afad404419 --- /dev/null +++ b/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"}]}]}}