# HG changeset patch
# User wenzelm
# Date 1761243218 -7200
# Node ID c262072aeabf8dc785cf3581168616ec203a69c9
# Parent  0e2e5adbdea5706a51c20f59ab0605199ea76cf1
tuned;

diff -r 0e2e5adbdea5 -r c262072aeabf 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)