--- a/src/Tools/VSCode/src/language_server.scala Fri Jun 27 12:25:06 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Fri Jun 27 13:24:05 2025 +0200
@@ -274,16 +274,15 @@
if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
}
- val resources =
+ val session_resources =
new VSCode_Resources(options, session_background, log) {
override def commit(change: Session.Change): Unit =
if (change.deps_changed || undefined_blobs(change.version).nonEmpty) {
delay_load.invoke()
}
}
-
val session_options = options.bool.update("editor_output_state", true)
- val session = new VSCode_Session(session_options, resources)
+ val session = new VSCode_Session(session_options, session_resources)
Some((session_background, session))
}