# HG changeset patch
# User wenzelm
# Date 1520689395 -3600
# Node ID 3e226d3b7bc69241765e11c54819341c254fc674
# Parent  b123c9a007d0c67722984fe9d75db35eadc5250b
adapted to 3869b2400e22;

diff -r b123c9a007d0 -r 3e226d3b7bc6 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Sat Mar 10 14:20:27 2018 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sat Mar 10 14:43:15 2018 +0100
@@ -616,7 +616,7 @@
     {
       val entries =
         for ((sym, code) <- Symbol.codes)
-        yield Map("symbol" -> sym, "name" -> Symbol.names(sym), "code" -> code)
+        yield Map("symbol" -> sym, "name" -> Symbol.names(sym)._1, "code" -> code)
       Notification("PIDE/symbols", Map("entries" -> entries))
     }
   }