--- a/src/Tools/VSCode/src/language_server.scala Sat Nov 01 14:32:12 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Sat Nov 01 14:34:26 2025 +0100
@@ -135,7 +135,7 @@
def resources: VSCode_Resources = session.resources
def ml_settings: ML_Settings = session.store.ml_settings
- private val sledgehammer = VSCode_Sledgehammer(server)
+ private val sledgehammer = new VSCode_Sledgehammer(server)
def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
for {
--- a/src/Tools/VSCode/src/vscode_sledgehammer.scala Sat Nov 01 14:32:12 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_sledgehammer.scala Sat Nov 01 14:34:26 2025 +0100
@@ -13,12 +13,7 @@
import java.io.{File => JFile}
-object VSCode_Sledgehammer {
- def apply(server: Language_Server): VSCode_Sledgehammer =
- new VSCode_Sledgehammer(server)
-}
-
-class VSCode_Sledgehammer private(server: Language_Server) {
+class VSCode_Sledgehammer(server: Language_Server) {
private val query_operation =
new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_output)