# 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) {