src/Tools/VSCode/src/server.scala
changeset 66211 100c9c997e2b
parent 66138 f7ef4c50b747
child 66215 9a8b6b86350c
--- a/src/Tools/VSCode/src/server.scala	Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu Jun 29 11:36:25 2017 +0200
@@ -450,6 +450,7 @@
           case Protocol.State_Exit(id) => State_Panel.exit(id)
           case Protocol.State_Locate(id) => State_Panel.locate(id)
           case Protocol.State_Update(id) => State_Panel.update(id)
+          case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
           case Protocol.Preview_Request(file, column) => request_preview(file, column)
           case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
           case _ => log("### IGNORED")