--- 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 })