src/Tools/VSCode/src/language_server.scala

   private val session_ = Synchronized(None: Option[VSCode_Session])
   def session: VSCode_Session = session_.value getOrElse error("Server inactive")
   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 {
       rendering <- resources.get_rendering(new JFile(node_pos.name))
       offset <- rendering.model.content.doc.offset(node_pos.pos)

 
       session.commands_changed += prover_output
       session.syslog_messages += syslog_messages
 
       dynamic_output.init()
-      sledgehammer_panel.init()
+      sledgehammer.init()
 
       try {
         Isabelle_Process.start(
           options, session, session_background, session_heaps, modes = modes).await_startup()
         reply_ok(

         file_watcher.shutdown()
         delay_input.revoke()
         delay_output.revoke()
         delay_caret_update.revoke()
         delay_preview.revoke()
-        sledgehammer_panel.exit()
+        sledgehammer.exit()
 
         val result = session.stop()
         if (result.ok) reply("")
         else reply("Prover shutdown failed: " + result.rc)
         None

           case LSP.Symbols_Convert_Request(id, text, boolean) =>
             symbols_convert_request(id, text, boolean)
           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")
         }
       }
       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     }