--- a/src/Tools/VSCode/src/language_server.scala Thu May 30 02:45:24 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Wed May 01 19:09:26 2024 +0200
@@ -442,10 +442,10 @@
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_Exit(id) => State_Panel.exit(id)
- case LSP.State_Locate(id) => State_Panel.locate(id)
- case LSP.State_Update(id) => State_Panel.update(id)
- case LSP.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
+ 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)
+ case LSP.State_Auto_Update(state_id, enabled) => State_Panel.auto_update(state_id, enabled)
case LSP.Preview_Request(file, column) => request_preview(file, column)
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}