lsp: added State_Init_Response message;
authorThomas Lindae <thomas.lindae@in.tum.de>
Wed, 24 Apr 2024 18:48:24 +0200
changeset 81021 89bfada3a16d
parent 81020 0efa8e784384
child 81022 4804614f25b3
lsp: added State_Init_Response message;
src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/lsp.scala	Thu May 30 02:43:16 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Wed Apr 24 18:48:24 2024 +0200
@@ -523,6 +523,11 @@
         JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update))
   }
 
+  object State_Init_Response {
+    def apply(id: Counter.ID): JSON.T =
+      Notification("PIDE/state_init_response", JSON.Object("id" -> id))
+  }
+
   class State_Id_Notification(name: String) {
     def unapply(json: JSON.T): Option[Counter.ID] =
       json match {
--- a/src/Tools/VSCode/src/state_panel.scala	Thu May 30 02:43:16 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Wed Apr 24 18:48:24 2024 +0200
@@ -18,6 +18,7 @@
     val instance = new State_Panel(server)
     instances.change(_ + (instance.id -> instance))
     instance.init()
+    instance.init_response()
   }
 
   def exit(id: Counter.ID): Unit = {
@@ -50,6 +51,9 @@
   private def output(content: String): Unit =
     server.channel.write(LSP.State_Output(id, content, auto_update_enabled.value))
 
+  private def init_response(): Unit =
+    server.channel.write(LSP.State_Init_Response(id))
+
 
   /* query operation */