changeset 67813 | 3e226d3b7bc6 |
parent 66675 | 6f4613dbfef6 |
child 67843 | ff561f6e0a8e |
--- 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)) } }