tuned;
authorwenzelm
Mon, 03 Nov 2025 12:59:56 +0100
changeset 83471 a435b581df12
parent 83470 347281fe2ac8
child 83472 2c5e82a84482
tuned;
src/Tools/VSCode/extension/src/lsp.ts
src/Tools/VSCode/src/lsp.scala
--- 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(