# HG changeset patch
# User wenzelm
# Date 1750791447 -7200
# Node ID ef9075e41a675e2441f03e268a6c8e4e83e7c511
# Parent  0ca8b1861fa30a646bd0c376c2680cef1073b6e3
tuned;

diff -r 0ca8b1861fa3 -r ef9075e41a67 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 })