# HG changeset patch
# User wenzelm
# Date 1761403190 -7200
# Node ID 485ba4e3787a1acd2acbc8821510d2fd081cde49
# Parent  b4cafd261b23aefa98f5e1cb14ac3f29b4aa37ba
clarified signature: more explicit types;

diff -r b4cafd261b23 -r 485ba4e3787a src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Sat Oct 25 14:46:29 2025 +0200
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sat Oct 25 16:39:50 2025 +0200
@@ -172,12 +172,19 @@
 export const documentation_request_type =
   new NotificationType<InitRequest>("PIDE/documentation_request")
 
+export interface Doc_Entry {
+  title: string;
+  path: string;
+}
+
+export interface Doc_Section {
+  title: string;
+  important: boolean;
+  entries: Array<Doc_Entry>;
+}
+
 export interface Documentation_Response {
-  sections: Array<{
-    title: string;
-    important: boolean;
-    entries: Array<{ title: string; path: string }>;
-  }>;
+  sections: Array<Doc_Section>;
 }
 
 export const documentation_response_type =
diff -r b4cafd261b23 -r 485ba4e3787a src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 14:46:29 2025 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 16:39:50 2025 +0200
@@ -792,21 +792,25 @@
       }
   }
 
+  object Doc_Entry {
+    def apply(entry: Doc.Entry): JSON.T =
+      JSON.Object("title" -> entry.title, "path" -> entry.path.toString)
+  }
+
+  object Doc_Section {
+    def apply(section: Doc.Section): JSON.T =
+      JSON.Object(
+        "title" -> section.title,
+        "important" -> section.important,
+        "entries" -> section.entries.map(Doc_Entry.apply))
+  }
+
   object Documentation_Response {
     def apply(): JSON.T = {
       val ml_settings = ML_Settings.init()
       val doc_contents = Doc.contents(ml_settings)
-      val json_sections = doc_contents.sections.map { section =>
-        JSON.Object(
-          "title" -> section.title,
-          "important" -> section.important,
-          "entries" -> section.entries.map { entry =>
-            JSON.Object("title" -> entry.title, "path" -> entry.path.toString)
-          }
-        )
-      }
-
-      Notification("PIDE/documentation_response", JSON.Object("sections" -> json_sections))
+      Notification("PIDE/documentation_response",
+        JSON.Object("sections" -> doc_contents.sections.map(Doc_Section.apply)))
     }
   }