# HG changeset patch # User Thomas Lindae # Date 1719852506 -7200 # Node ID 84f6f17274d091f04a498ae5c0315ef99f3a90a7 # Parent a9dc66e0529730f8d10584c7d80264af7a9e6eef lsp: changed State_Init notification into a request and removed State_Init_Response; diff -r a9dc66e05297 -r 84f6f17274d0 src/Tools/VSCode/src/language_server.scala --- 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) diff -r a9dc66e05297 -r 84f6f17274d0 src/Tools/VSCode/src/lsp.scala --- 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") diff -r a9dc66e05297 -r 84f6f17274d0 src/Tools/VSCode/src/state_panel.scala --- 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 */