# HG changeset patch
# User wenzelm
# Date 1762123265 -3600
# Node ID e7c174e335568883767418d0fb80cf1483961b9c
# Parent  b6916f2ff67244e0d8873db8f1dc1c62d9c6d375
clarified names;

diff -r b6916f2ff672 -r e7c174e33556 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Sun Nov 02 23:31:57 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sun Nov 02 23:41:05 2025 +0100
@@ -156,12 +156,12 @@
   abbrevs_from_Thy: [string, string][];
 }
 
+export const symbols_request_type =
+  new NotificationType<void>("PIDE/symbols_request")
+
 export const symbols_response_type =
   new NotificationType<Symbols_Response>("PIDE/symbols_response");
 
-export const symbols_panel_request_type =
-  new NotificationType<void>("PIDE/symbols_panel_request")
-
 
 /* documentation */
 
diff -r b6916f2ff672 -r e7c174e33556 src/Tools/VSCode/extension/src/symbol_panel.ts
--- a/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Nov 02 23:31:57 2025 +0100
+++ b/src/Tools/VSCode/extension/src/symbol_panel.ts	Sun Nov 02 23:41:05 2025 +0100
@@ -31,7 +31,7 @@
 
   request( language_client: LanguageClient) {
     if (language_client) {
-      this._language_client.sendNotification(lsp.symbols_panel_request_type);
+      this._language_client.sendNotification(lsp.symbols_request_type);
     }
   }
 
diff -r b6916f2ff672 -r e7c174e33556 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 23:31:57 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Sun Nov 02 23:41:05 2025 +0100
@@ -476,7 +476,7 @@
     channel.write(LSP.Symbols_Convert_Request.reply(id, converted))
   }
 
-  def symbols_panel_request(): Unit = {
+  def symbols_request(): Unit = {
     val abbrevs =
       resources.get_caret().flatMap { caret =>
         resources.get_model(caret.file).map(_.syntax().abbrevs)
@@ -531,7 +531,7 @@
           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() => symbols_panel_request()
+          case LSP.Symbols_Request() => symbols_request()
           case LSP.Documentation_Request() => documentation_request()
           case LSP.Sledgehammer_Provers_Request() => sledgehammer.provers()
           case LSP.Sledgehammer_Request(args) => sledgehammer.request(args)
diff -r b6916f2ff672 -r e7c174e33556 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sun Nov 02 23:31:57 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Sun Nov 02 23:41:05 2025 +0100
@@ -720,8 +720,8 @@
       ResponseMessage(id, Some(JSON.Object("text" -> new_string)))
   }
 
-  object Symbols_Panel_Request
-    extends Notification0("PIDE/symbols_panel_request")
+  object Symbols_Request
+    extends Notification0("PIDE/symbols_request")
 
   object Symbols_Response {
     def apply(symbols: Symbol.Symbols, abbrevs: List[(String, String)]): JSON.T = {