# HG changeset patch
# User wenzelm
# Date 1762165911 -3600
# Node ID 80908b334dc7b4d09eb3c676473cc6da10e5ef2b
# Parent  974a67c6cc310ffc21efac79d5a1a8d95ce020f5
tuned;

diff -r 974a67c6cc31 -r 80908b334dc7 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 11:20:51 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Mon Nov 03 11:31:51 2025 +0100
@@ -717,23 +717,21 @@
 
   object Symbols_Response {
     def apply(symbols: Symbol.Symbols, abbrevs: List[(String, String)]): JSON.T = {
-      def json(symbol: Symbol.Entry): JSON.T = {
-        val decoded = Symbol.decode(symbol.symbol)
+      def symbol(entry: Symbol.Entry): JSON.T = {
         JSON.Object(
-          "symbol" -> symbol.symbol,
-          "name" -> symbol.name,
-          "argument" -> symbol.argument.toString,
-          "decoded" -> decoded) ++
-        JSON.optional("code", symbol.code) ++
-        JSON.optional("font", symbol.font) ++
+          "symbol" -> entry.symbol,
+          "name" -> entry.name,
+          "argument" -> entry.argument.toString,
+          "decoded" -> Symbol.decode(entry.symbol)) ++
+        JSON.optional("code", entry.code) ++
+        JSON.optional("font", entry.font) ++
         JSON.Object(
-          "groups" -> symbol.groups,
-          "abbrevs" -> symbol.abbrevs)
+          "groups" -> entry.groups,
+          "abbrevs" -> entry.abbrevs)
       }
-
       Notification("PIDE/symbols_response",
         JSON.Object(
-          "symbols" -> symbols.entries.map(json),
+          "symbols" -> symbols.entries.map(symbol),
           "abbrevs_from_Thy" -> (for ((a, b) <- abbrevs) yield List(a, b))))
     }
   }