# HG changeset patch
# User wenzelm
# Date 1762171551 -3600
# Node ID 2c5e82a844828361d28c167a695b99ceb885cb52
# Parent  a435b581df128ee181b680a205935ed7d74dba6d
unused (see also f0341e6b1b30);

diff -r a435b581df12 -r 2c5e82a84482 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Mon Nov 03 12:59:56 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Nov 03 13:05:51 2025 +0100
@@ -471,11 +471,6 @@
 
   /* 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))
-  }
-
   def symbols_request(): Unit = {
     val syntax =
       resources.get_caret().map(_.model.syntax())
@@ -526,8 +521,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_Convert_Request(id, text, boolean) =>
-            symbols_convert_request(id, text, boolean)
           case LSP.Preview_Request(file, column) => preview_request(file, column)
           case LSP.Symbols_Request() => symbols_request()
           case LSP.Documentation_Request() => documentation_request()
diff -r a435b581df12 -r 2c5e82a84482 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 12:59:56 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 13:05:51 2025 +0100
@@ -697,21 +697,6 @@
 
   /* symbols */
 
-  object Symbols_Convert_Request {
-    def unapply(json: JSON.T): Option[(Id, String, Boolean)] =
-      json match {
-        case RequestMessage(id, "PIDE/symbols_convert_request", Some(params)) =>
-          for {
-            text <- JSON.string(params, "text")
-            unicode <- JSON.bool(params, "unicode")
-          } yield (id, text, unicode)
-        case _ => None
-      }
-
-    def reply(id: Id, new_string: String): JSON.T =
-      ResponseMessage(id, Some(JSON.Object("text" -> new_string)))
-  }
-
   object Symbols_Request
     extends Notification0("PIDE/symbols_request")