src/Tools/VSCode/src/lsp.scala

--- a/src/Tools/VSCode/src/lsp.scala	Thu May 09 22:22:44 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Thu May 09 23:05:10 2024 +0200
@@ -586,6 +586,29 @@
   }
 
 
+  /* symbols */
+
+  object Symbols_Request extends Request0("PIDE/symbols_request") {
+    def reply(id: Id, symbols: Symbol.Symbols): JSON.T = {
+      def json(symbol: Symbol.Entry): JSON.T =
+        JSON.Object(
+          "symbol" -> symbol.symbol,
+          "name" -> symbol.name,
+          "argument" -> symbol.argument.toString,
+        ) ++
+          JSON.optional("code", symbol.code) ++
+          JSON.optional("font", symbol.font) ++
+          JSON.Object(
+            "groups" -> symbol.groups,
+            "abbrevs" -> symbol.abbrevs,
+          )
+
+      ResponseMessage(id, Some(symbols.entries.map(s => json(s))))
+    }
+
+  }
+
+
   /* preview */
 
   object Preview_Request {