lsp: added Symbols_Request;

--- a/src/Tools/VSCode/src/language_server.scala	Thu May 09 22:22:44 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Thu May 09 23:05:10 2024 +0200
@@ -413,6 +413,14 @@
   }
 
 
+  /* symbols */
+
+  def symbols_request(id: LSP.Id): Unit = {
+    val symbols = Component_VSCodium.symbols
+    channel.write(LSP.Symbols_Request.reply(id, symbols))
+  }
+
+
   /* main loop */
 
   def start(): Unit = {
@@ -448,6 +456,7 @@
           case LSP.State_Update(state_id) => State_Panel.update(state_id)
           case LSP.State_Auto_Update(state_id, enabled) => State_Panel.auto_update(state_id, enabled)
           case LSP.State_Set_Margin(state_id, margin) => State_Panel.set_margin(state_id, margin)
+          case LSP.Symbols_Request(id) => symbols_request(id)
           case LSP.Preview_Request(file, column) => request_preview(file, column)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }

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