src/Tools/VSCode/src/server.scala

--- a/src/Tools/VSCode/src/server.scala	Fri Jun 09 16:59:14 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Fri Jun 09 17:13:50 2017 +0200
@@ -398,6 +398,7 @@
           case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
           case Protocol.Caret_Update(caret) => update_caret(caret)
           case Protocol.Preview_Request(file, column) => request_preview(file, column)
+          case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
           case _ => log("### IGNORED")
         }
       }