# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1720536468 -7200
# Node ID f0341e6b1b306bb85e8bf1f07ec8ae652fce2ecc
# Parent  c87d2fa560ddf49f601da9794acea84aa1980bbf
lsp: added symbol conversion request;

diff -r c87d2fa560dd -r f0341e6b1b30 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Fri Jul 05 21:40:39 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Jul 09 16:47:48 2024 +0200
@@ -486,6 +486,11 @@
     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))
+  }
 
 
   /* main loop */
@@ -526,6 +531,7 @@
           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)
           case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
         }
diff -r c87d2fa560dd -r f0341e6b1b30 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Fri Jul 05 21:40:39 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Tue Jul 09 16:47:48 2024 +0200
@@ -668,7 +668,21 @@
 
       ResponseMessage(id, Some(symbols.entries.map(s => json(s))))
     }
+  }
+  
+  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 {
+            s <- JSON.string(params, "text")
+            unicode <- JSON.bool(params, "unicode")
+          } yield (id, s, unicode)
+        case _ => None
+      }
 
+    def reply(id: Id, new_string: String): JSON.T =
+      ResponseMessage(id, Some(JSON.Object("text" -> new_string)))
   }