discontinue pointless "init" flag;
authorwenzelm
Sun, 26 Oct 2025 20:46:09 +0100
changeset 83406 9b3a9d739c2e
parent 83405 6ac2c6c2e549
child 83407 a51835dd6a64
discontinue pointless "init" flag;
src/Tools/VSCode/extension/src/documentation_panel.ts
src/Tools/VSCode/extension/src/lsp.ts
src/Tools/VSCode/extension/src/symbol_panel.ts
src/Tools/VSCode/src/language_server.scala
src/Tools/VSCode/src/lsp.scala
--- 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 = {