tuned: avoid overlapping scopes;
authorwenzelm
Fri, 27 Jun 2025 13:24:05 +0200
changeset 82777 86a9aaa92877
parent 82776 d2e401f7d364
child 82778 803731b62180
tuned: avoid overlapping scopes;
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))
       }