# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1719801244 -7200
# Node ID 54bda6e0e848f0c4c80860f7e93b605b10f9de60
# Parent  6823aaab3c844b439917ea546b231797a3ad0850
lsp: added rudimentary indenting to code actions;

diff -r 6823aaab3c84 -r 54bda6e0e848 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Jul 01 18:53:27 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Jul 01 04:34:04 2024 +0200
@@ -454,13 +454,17 @@
               range = command.core_range + start
               current_text <- doc.get_text(range)
               line_range = doc.range(range)
+
+              whole_line = doc.lines(line_range.start.line)
+              indent = whole_line.text.takeWhile(_.isWhitespace)
               padding = p.contains(Markup.PADDING_COMMAND)
-            } yield {
-              val edit_text =
-                resources.output_edit(if (padding) current_text + "\n" + s else current_text + s)
-              val edit = LSP.TextEdit(line_range, edit_text)
-              (s, edit)
-            }
+
+              indented_text = Library.prefix_lines(indent, s)
+              edit_text =
+                resources.output_edit(
+                  if (padding) current_text + "\n" + indented_text else current_text + s)
+              edit = LSP.TextEdit(line_range, edit_text)
+            } yield (s, edit) 
         })
         .distinct