src/Tools/VSCode/src/lsp.scala

--- a/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 19:52:22 2025 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 19:54:47 2025 +0200
@@ -787,7 +787,9 @@
 
   object Doc_Entry {
     def apply(entry: Doc.Entry): JSON.T =
-      JSON.Object("title" -> entry.title, "path" -> entry.path.toString)
+      JSON.Object(
+        "print_html" -> entry.print_html,
+        "platform_path" -> File.platform_path(entry.path))
   }
 
   object Doc_Section {