# HG changeset patch
# User wenzelm
# Date 1761483991 -3600
# Node ID 715a6441422fcf856db85fcd99192e3eeb141ab9
# Parent  5248a91e91fbff5246cc352e954c5d7378928489
unused;

diff -r 5248a91e91fb -r 715a6441422f src/Tools/VSCode/src/vscode_sledgehammer.scala
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 13:57:17 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala	Sun Oct 26 14:06:31 2025 +0100
@@ -7,7 +7,7 @@
 
 import isabelle._
 
-import java.io.{PrintStream, PrintWriter, FileWriter, OutputStream, File => JFile}
+import java.io.{File => JFile}
 
 
 object VSCode_Sledgehammer {
@@ -156,8 +156,6 @@
       val query_position = sendback_id_opt.flatMap(id => query_position_from_sendback(snapshot, id))
         .getOrElse(("unknown", 0, 0))
 
-      val text = snapshot.node.source
-
       val json = JSON.Object(
         "content" -> xml_string,
         "position" -> JSON.Object(