--- 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 */