# HG changeset patch
# User wenzelm
# Date 1751023445 -7200
# Node ID 86a9aaa92877292cbbf7c0bd92c51c306add999b
# Parent  d2e401f7d364e4c2afa7617f1a4b4cf345247d6b
tuned: avoid overlapping scopes;

diff -r d2e401f7d364 -r 86a9aaa92877 src/Tools/VSCode/src/language_server.scala
--- 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))
       }