# HG changeset patch
# User wenzelm
# Date 1761411932 -7200
# Node ID 81a832cab4e286dffcd0e5def44815ee7b67382e
# Parent  e7e1ffa36821a9176743b3700c603ad80c923775
misc tuning;

diff -r e7e1ffa36821 -r 81a832cab4e2 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sat Oct 25 17:27:33 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Oct 25 19:05:32 2025 +0200
@@ -118,7 +118,7 @@
   def resources: VSCode_Resources = session.resources
   def ml_settings: ML_Settings = session.store.ml_settings
 
-  private val sledgehammer_panel = VSCode_Sledgehammer(server)
+  private val sledgehammer = VSCode_Sledgehammer(server)
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
@@ -298,7 +298,7 @@
       session.syslog_messages += syslog_messages
 
       dynamic_output.init()
-      sledgehammer_panel.init()
+      sledgehammer.init()
 
       try {
         Isabelle_Process.start(
@@ -327,7 +327,7 @@
         delay_output.revoke()
         delay_caret_update.revoke()
         delay_preview.revoke()
-        sledgehammer_panel.exit()
+        sledgehammer.exit()
 
         val result = session.stop()
         if (result.ok) reply("")
@@ -549,10 +549,12 @@
           case LSP.Preview_Request(file, column) => preview_request(file, column)
           case LSP.Symbols_Panel_Request(init) => symbols_panel_request(init)
           case LSP.Documentation_Request(init) => documentation_request(init)
-          case LSP.Sledgehammer_Request(provers, isar, try0, purpose) => sledgehammer_panel.handle_request(provers, isar, try0, purpose)
-          case LSP.Sledgehammer_Cancel => sledgehammer_panel.cancel_query()
-          case LSP.Sledgehammer_Provers(init) => sledgehammer_panel.send_provers_and_history(init)
-          case LSP.Sledgehammer_Delete_Prover(entry) => sledgehammer_panel.handle_sledgehammer_delete(entry)
+          case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
+            sledgehammer.handle_request(provers, isar, try0, purpose)
+          case LSP.Sledgehammer_Cancel => sledgehammer.cancel_query()
+          case LSP.Sledgehammer_Provers(init) => sledgehammer.send_provers_and_history(init)
+          case LSP.Sledgehammer_Delete_Prover(entry) =>
+            sledgehammer.handle_sledgehammer_delete(entry)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
       }