fix: indent #guard_msgs code action to match command indentation

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⟩

tests/server_interactive/guardMsgsCodeActionIndent.lean

@@ -0,0 +1,5 @@
+namespace Foo
+  #guard_msgs in
+  --^ codeAction
+  #eval 0
+end Foo

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  "}]}]}}

tests/server_interactive/guardMsgsCodeActionIndentMulti.lean

@@ -0,0 +1,5 @@
+namespace Foo
+  #guard_msgs in
+  --^ codeAction
+  #eval IO.println "a\nb"
+end Foo

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  "}]}]}}