# HG changeset patch
# User wenzelm
# Date 1762122717 -3600
# Node ID b6916f2ff67244e0d8873db8f1dc1c62d9c6d375
# Parent  fca677fc8a3559d9c71ef1579f81bb89f73e4e7c
unused (see also 88879ff1cef5);

diff -r fca677fc8a35 -r b6916f2ff672 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 23:23:00 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 23:31:57 2025 +0100
@@ -471,11 +471,6 @@
 
   /* symbols */
 
-  def symbols_request(id: LSP.Id): Unit = {
-    val symbols = Component_VSCodium.symbols
-    channel.write(LSP.Symbols_Request.reply(id, symbols))
-  }
-  
   def symbols_convert_request(id: LSP.Id, text: String, unicode: Boolean): Unit = {
     val converted = Symbol.output(unicode, text)
     channel.write(LSP.Symbols_Convert_Request.reply(id, converted))
@@ -533,7 +528,6 @@
           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.Symbols_Convert_Request(id, text, boolean) =>
             symbols_convert_request(id, text, boolean)
           case LSP.Preview_Request(file, column) => preview_request(file, column)
diff -r fca677fc8a35 -r b6916f2ff672 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sun Nov 02 23:23:00 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Nov 02 23:31:57 2025 +0100
@@ -705,23 +705,6 @@
 
   /* 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))))
-    }
-  }
-
   object Symbols_Convert_Request {
     def unapply(json: JSON.T): Option[(Id, String, Boolean)] =
       json match {