--- a/src/Tools/VSCode/extension/src/documentation_panel.ts Sun Oct 26 19:38:38 2025 +0100
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts Sun Oct 26 20:46:09 2025 +0100
@@ -30,8 +30,7 @@
request(language_client: LanguageClient) {
if (language_client) {
- this._language_client.sendNotification(lsp.documentation_request_type, { init: true });
-
+ this._language_client.sendNotification(lsp.documentation_request_type);
}
}
--- a/src/Tools/VSCode/extension/src/lsp.ts Sun Oct 26 19:38:38 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts Sun Oct 26 20:46:09 2025 +0100
@@ -159,18 +159,14 @@
export const symbols_response_type =
new NotificationType<Symbols_Response>("PIDE/symbols_response");
-export interface InitRequest {
- init: boolean;
-}
-
export const symbols_request_type =
- new NotificationType<InitRequest>("PIDE/symbols_panel_request")
+ new NotificationType<void>("PIDE/symbols_panel_request")
/* documentation */
export const documentation_request_type =
- new NotificationType<InitRequest>("PIDE/documentation_request")
+ new NotificationType<void>("PIDE/documentation_request")
export interface Doc_Entry {
print_html: string;
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts Sun Oct 26 19:38:38 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts Sun Oct 26 20:46:09 2025 +0100
@@ -31,7 +31,7 @@
request( language_client: LanguageClient) {
if (language_client) {
- this._language_client.sendNotification(lsp.symbols_request_type, { init: true });
+ this._language_client.sendNotification(lsp.symbols_request_type);
}
}
--- a/src/Tools/VSCode/src/language_server.scala Sun Oct 26 19:38:38 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Sun Oct 26 20:46:09 2025 +0100
@@ -491,7 +491,7 @@
channel.write(LSP.Symbols_Convert_Request.reply(id, converted))
}
- def symbols_panel_request(init: Boolean): Unit = {
+ def symbols_panel_request(): Unit = {
val abbrevs =
resources.get_caret().flatMap { caret =>
resources.get_model(caret.file).map(_.syntax().abbrevs)
@@ -501,7 +501,7 @@
}
- def documentation_request(init: Boolean): Unit =
+ def documentation_request(): Unit =
channel.write(LSP.Documentation_Response(ml_settings))
@@ -547,8 +547,8 @@
case LSP.Symbols_Convert_Request(id, text, boolean) =>
symbols_convert_request(id, text, boolean)
case LSP.Preview_Request(file, column) => preview_request(file, column)
- case LSP.Symbols_Panel_Request(init) => symbols_panel_request(init)
- case LSP.Documentation_Request(init) => documentation_request(init)
+ case LSP.Symbols_Panel_Request => symbols_panel_request()
+ case LSP.Documentation_Request => documentation_request()
case LSP.Sledgehammer_Request(provers, isar, try0, purpose) =>
sledgehammer.handle_request(provers, isar, try0, purpose)
case LSP.Sledgehammer_Cancel => sledgehammer.cancel_query()
--- a/src/Tools/VSCode/src/lsp.scala Sun Oct 26 19:38:38 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Sun Oct 26 20:46:09 2025 +0100
@@ -741,14 +741,8 @@
ResponseMessage(id, Some(JSON.Object("text" -> new_string)))
}
- object Symbols_Panel_Request {
- def unapply(json: JSON.T): Option[Boolean] =
- json match {
- case Notification("PIDE/symbols_panel_request", Some(params)) =>
- JSON.bool(params, "init")
- case _ => None
- }
- }
+ object Symbols_Panel_Request
+ extends Notification0("PIDE/symbols_panel_request")
object Symbols_Response {
def apply(symbols: Symbol.Symbols, abbrevs: List[(String, String)]): JSON.T = {