tuned;
authorwenzelm
Thu, 23 Oct 2025 20:13:38 +0200
changeset 83372 c262072aeabf
parent 83371 0e2e5adbdea5
child 83373 9e59028314be
tuned;
src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Thu Oct 23 20:09:14 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Thu Oct 23 20:13:38 2025 +0200
@@ -105,7 +105,7 @@
     snapshot.node.commands.find(_.id == sendbackId).flatMap { command =>
       snapshot.node.command_iterator().find(_._1 == command).map {
         case (_, start_offset) =>
-          val end_offset = start_offset + command.length // Hier nehmen wir das Ende des Command!
+          val end_offset = start_offset + command.length
           val text = snapshot.node.source
           val line = count_lines(text, end_offset)
           val column = count_column(text, end_offset)