--- a/src/Tools/VSCode/src/protocol.scala Wed Jun 28 14:17:05 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala Thu Jun 29 11:36:25 2017 +0200
@@ -528,6 +528,19 @@
object State_Locate extends State_Id_Notification("PIDE/state_locate")
object State_Update extends State_Id_Notification("PIDE/state_update")
+ object State_Auto_Update
+ {
+ def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] =
+ json match {
+ case Notification("PIDE/state_auto_update", Some(params)) =>
+ for {
+ id <- JSON.long(params, "id")
+ enabled <- JSON.bool(params, "enabled")
+ } yield (id, enabled)
+ case _ => None
+ }
+ }
+
/* preview */