--- 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 */