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