tuned;
authorwenzelm
Tue, 24 Jun 2025 20:57:27 +0200
changeset 82745 ef9075e41a67
parent 82744 0ca8b1861fa3
child 82746 535e6012ee11
tuned;
src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 24 20:52:09 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 24 20:57:27 2025 +0200
@@ -264,7 +264,7 @@
     range: Symbol.Range
   ): Option[Line.Node_Range] = {
     for {
-      platform_path <- resources.source_file(model.session.resources.ml_settings, source_name)
+      platform_path <- resources.source_file(resources.ml_settings, source_name)
       file <-
         (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })