# HG changeset patch
# User wenzelm
# Date 1761404773 -7200
# Node ID 93a03569641837aae8bddb576efdff879d87116d
# Parent  f5ddeb30954067abe27ab562afe8accd80ecbf17
proper ml_settings, following Isabelle/jEdit;

diff -r f5ddeb309540 -r 93a035696418 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sat Oct 25 16:57:34 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Oct 25 17:06:13 2025 +0200
@@ -116,6 +116,8 @@
   private val session_ = Synchronized(None: Option[VSCode_Session])
   def session: VSCode_Session = session_.value getOrElse error("Server inactive")
   def resources: VSCode_Resources = session.resources
+  def ml_settings: ML_Settings = session.store.ml_settings
+
   private val sledgehammer_panel = VSCode_Sledgehammer(this)
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
@@ -499,9 +501,8 @@
   }
 
 
-  def documentation_request(init: Boolean): Unit = {
-    channel.write(LSP.Documentation_Response())
-  }
+  def documentation_request(init: Boolean): Unit =
+    channel.write(LSP.Documentation_Response(ml_settings))
 
 
   /* main loop */
diff -r f5ddeb309540 -r 93a035696418 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 16:57:34 2025 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 17:06:13 2025 +0200
@@ -799,8 +799,7 @@
   }
 
   object Documentation_Response {
-    def apply(): JSON.T = {
-      val ml_settings = ML_Settings.init()
+    def apply(ml_settings: ML_Settings): JSON.T = {
       val doc_contents = Doc.contents(ml_settings)
       Notification("PIDE/documentation_response",
         JSON.Object("sections" -> doc_contents.sections.map(Doc_Section.apply)))