# HG changeset patch
# User wenzelm
# Date 1750844768 -7200
# Node ID 9fea73244f06fff92fa1fb9f56564666a9310ebe
# Parent  c3c8e84f63c62a4546a24389dc93641366e478d0
clarified signature: avoid duplicate ML_Settings.system;

diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -58,7 +58,7 @@
     server.session.caret_focus += main
     pretty_panel_.change(_ =>
       Some(Pretty_Text_Panel(
-        server.resources,
+        server.session,
         server.channel,
         LSP.Dynamic_Output.apply)))
     handle_update(None)
diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -274,10 +274,8 @@
           if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
         }
 
-        val ml_settings = ML_Settings.system(options)
-
         val resources =
-          new VSCode_Resources(options, ml_settings, session_background, log) {
+          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()
diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/pretty_text_panel.scala
--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -12,14 +12,14 @@
 
 object Pretty_Text_Panel {
   def apply(
-    resources: VSCode_Resources,
+    session: VSCode_Session,
     channel: Channel,
     output: (String, Option[LSP.Decoration]) => JSON.T
-  ): Pretty_Text_Panel = new Pretty_Text_Panel(resources, channel, output)
+  ): Pretty_Text_Panel = new Pretty_Text_Panel(session, channel, output)
 }
 
 class Pretty_Text_Panel private(
-  resources: VSCode_Resources,
+  session: VSCode_Session,
   channel: Channel,
   output_json: (String, Option[LSP.Decoration]) => JSON.T
 ) {
@@ -31,6 +31,8 @@
     refresh(current_output)
   }
 
+  def resources: VSCode_Resources = session.resources
+
   def update_margin(new_margin: Double): Unit = {
     margin = new_margin
     delay_margin.invoke()
@@ -51,7 +53,7 @@
               for {
                 thy_file <- Position.Def_File.unapply(props)
                 def_line <- Position.Def_Line.unapply(props)
-                platform_path <- resources.source_file(resources.ml_settings, thy_file)
+                platform_path <- resources.source_file(session.store.ml_settings, thy_file)
                 uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
               } yield HTML.link(uri.toString + "#" + def_line, body)
           }
diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -62,7 +62,7 @@
   private val output_active = Synchronized(true)
   private val pretty_panel =
     Synchronized(Pretty_Text_Panel(
-      server.resources,
+      server.session,
       server.channel,
       (content, decorations) =>
         LSP.State_Output(id, content, auto_update_enabled.value, decorations)
diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -264,7 +264,7 @@
     range: Symbol.Range
   ): Option[Line.Node_Range] = {
     for {
-      platform_path <- resources.source_file(resources.ml_settings, source_name)
+      platform_path <- resources.source_file(model.session.store.ml_settings, source_name)
       file <-
         (try { Some(File.absolute(new JFile(platform_path))) }
          catch { case ERROR(_) => None })
diff -r c3c8e84f63c6 -r 9fea73244f06 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 24 22:30:49 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Jun 25 11:46:08 2025 +0200
@@ -69,7 +69,6 @@
 
 class VSCode_Resources(
   val options: Options,
-  val ml_settings: ML_Settings,
   session_background: Sessions.Background,
   log: Logger = new Logger)
 extends Resources(session_background, log = log) {