diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index 2d30fd9b83e9..660ef7164611 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -264,13 +264,14 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do lazy? := some do let some start := stx.getPos? true | return eager let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager + let indent := "".pushn ' ' (doc.meta.text.toPosition start).column let res := revealTrailingWhitespace res let newText := if res.isEmpty then "" else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length? - s!"/-- {res} -/\n" + s!"/-- {res} -/\n{indent}" else - s!"/--\n{res}\n-/\n" + s!"/--\n{res}\n{indent}-/\n{indent}" pure { eager with edit? := some <|.ofTextEdit doc.versionedIdentifier { range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩ diff --git a/tests/server_interactive/guardMsgsCodeActionIndent.lean b/tests/server_interactive/guardMsgsCodeActionIndent.lean new file mode 100644 index 000000000000..1356d2b5a343 --- /dev/null +++ b/tests/server_interactive/guardMsgsCodeActionIndent.lean @@ -0,0 +1,5 @@ +namespace Foo + #guard_msgs in + --^ codeAction + #eval 0 +end Foo diff --git a/tests/server_interactive/guardMsgsCodeActionIndent.lean.out.expected b/tests/server_interactive/guardMsgsCodeActionIndent.lean.out.expected new file mode 100644 index 000000000000..70bdb116d8f7 --- /dev/null +++ b/tests/server_interactive/guardMsgsCodeActionIndent.lean.out.expected @@ -0,0 +1,28 @@ +{"textDocument": {"uri": "file:///guardMsgsCodeActionIndent.lean"}, + "range": + {"start": {"line": 1, "character": 4}, "end": {"line": 1, "character": 4}}, + "context": {"diagnostics": []}} +[{"title": "Update #guard_msgs with generated message", + "kind": "quickfix", + "isPreferred": true, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.cmdCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///guardMsgsCodeActionIndent.lean"}, + "range": + {"start": {"line": 1, "character": 4}, "end": {"line": 1, "character": 4}}, + "context": {"diagnostics": []}}}}] +Resolution of Update #guard_msgs with generated message: +{"title": "Update #guard_msgs with generated message", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///guardMsgsCodeActionIndent.lean"}, + "edits": + [{"range": + {"start": {"line": 1, "character": 2}, + "end": {"line": 1, "character": 2}}, + "newText": "/-- info: 0 -/\n "}]}]}} diff --git a/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean b/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean new file mode 100644 index 000000000000..4ab667bbb02a --- /dev/null +++ b/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean @@ -0,0 +1,5 @@ +namespace Foo + #guard_msgs in + --^ codeAction + #eval IO.println "a\nb" +end Foo diff --git a/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean.out.expected b/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean.out.expected new file mode 100644 index 000000000000..ec7a481e3c97 --- /dev/null +++ b/tests/server_interactive/guardMsgsCodeActionIndentMulti.lean.out.expected @@ -0,0 +1,28 @@ +{"textDocument": {"uri": "file:///guardMsgsCodeActionIndentMulti.lean"}, + "range": + {"start": {"line": 1, "character": 4}, "end": {"line": 1, "character": 4}}, + "context": {"diagnostics": []}} +[{"title": "Update #guard_msgs with generated message", + "kind": "quickfix", + "isPreferred": true, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.cmdCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///guardMsgsCodeActionIndentMulti.lean"}, + "range": + {"start": {"line": 1, "character": 4}, "end": {"line": 1, "character": 4}}, + "context": {"diagnostics": []}}}}] +Resolution of Update #guard_msgs with generated message: +{"title": "Update #guard_msgs with generated message", + "kind": "quickfix", + "isPreferred": true, + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///guardMsgsCodeActionIndentMulti.lean"}, + "edits": + [{"range": + {"start": {"line": 1, "character": 2}, + "end": {"line": 1, "character": 2}}, + "newText": "/--\ninfo: a\nb\n -/\n "}]}]}}