--- a/src/Tools/VSCode/extension/src/lsp.ts Mon Nov 03 11:42:48 2025 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts Mon Nov 03 12:59:56 2025 +0100
@@ -141,14 +141,14 @@
/* symbols */
export interface Symbol_Entry {
+ symbol: string;
name: string;
+ decoded: string;
+ argument: string;
abbrevs: string[];
groups: string[];
code?: number;
font?: string;
- symbol: string;
- argument: string;
- decoded: string;
}
export interface Symbols_Response {
--- a/src/Tools/VSCode/src/lsp.scala Mon Nov 03 11:42:48 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Mon Nov 03 12:59:56 2025 +0100
@@ -721,13 +721,12 @@
JSON.Object(
"symbol" -> entry.symbol,
"name" -> entry.name,
+ "decoded" -> Symbol.decode(entry.symbol),
"argument" -> entry.argument.toString,
- "decoded" -> Symbol.decode(entry.symbol)) ++
+ "groups" -> entry.groups,
+ "abbrevs" -> entry.abbrevs) ++
JSON.optional("code", entry.code) ++
- JSON.optional("font", entry.font) ++
- JSON.Object(
- "groups" -> entry.groups,
- "abbrevs" -> entry.abbrevs)
+ JSON.optional("font", entry.font)
}
Notification("PIDE/symbols_response",
JSON.Object(