# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1713977304 -7200
# Node ID 89bfada3a16d404af0ed17108f803f234cd2d043
# Parent  0efa8e784384f154f50a9faee68fe4cbeb95f45a
lsp: added State_Init_Response message;

diff -r 0efa8e784384 -r 89bfada3a16d src/Tools/VSCode/src/lsp.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 {
diff -r 0efa8e784384 -r 89bfada3a16d src/Tools/VSCode/src/state_panel.scala
--- 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 */