lsp: changed State_Init notification into a request and removed State_Init_Response;

--- a/src/Tools/VSCode/src/language_server.scala	Wed May 01 19:09:26 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Jul 01 18:48:26 2024 +0200
@@ -441,7 +441,7 @@
           case LSP.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case LSP.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
           case LSP.Caret_Update(caret) => update_caret(caret)
-          case LSP.State_Init(()) => State_Panel.init(server)
+          case LSP.State_Init(id) => State_Panel.init(id, server)
           case LSP.State_Exit(state_id) => State_Panel.exit(state_id)
           case LSP.State_Locate(state_id) => State_Panel.locate(state_id)
           case LSP.State_Update(state_id) => State_Panel.update(state_id)

--- a/src/Tools/VSCode/src/lsp.scala	Wed May 01 19:09:26 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Jul 01 18:48:26 2024 +0200
@@ -533,11 +533,6 @@
         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 {
@@ -546,7 +541,11 @@
       }
   }
 
-  object State_Init extends Notification0("PIDE/state_init")
+  object State_Init extends Request0("PIDE/state_init") {
+    def reply(id: Id, state_id: Counter.ID): JSON.T =
+      ResponseMessage(id, Some(JSON.Object("state_id" -> state_id)))
+  }
+
   object State_Exit extends State_Id_Notification("PIDE/state_exit")
   object State_Locate extends State_Id_Notification("PIDE/state_locate")
   object State_Update extends State_Id_Notification("PIDE/state_update")

--- a/src/Tools/VSCode/src/state_panel.scala	Wed May 01 19:09:26 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Mon Jul 01 18:48:26 2024 +0200
@@ -14,11 +14,11 @@
   private val make_id = Counter.make()
   private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
 
-  def init(server: Language_Server): Unit = {
+  def init(id: LSP.Id, server: Language_Server): Unit = {
     val instance = new State_Panel(server)
     instances.change(_ + (instance.id -> instance))
     instance.init()
-    instance.init_response()
+    instance.init_response(id)
   }
 
   def exit(id: Counter.ID): Unit = {
@@ -52,8 +52,8 @@
   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))
+  private def init_response(id: LSP.Id): Unit =
+    server.channel.write(LSP.State_Init.reply(id, this.id))
 
 
   /* query operation */