diff -r 78a1aedd1761 -r 6187612e83c1 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Fri Jun 16 16:00:44 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Fri Jun 16 16:21:17 2017 +0200 @@ -467,6 +467,29 @@ } + /* state output */ + + object State_Output + { + def apply(id: Counter.ID, content: String): JSON.T = + Notification("PIDE/state_output", Map("id" -> id, "content" -> content)) + } + + class State_Id_Notification(name: String) + { + def unapply(json: JSON.T): Option[Counter.ID] = + json match { + case Notification(method, Some(params)) if method == name => JSON.long(params, "id") + case _ => None + } + } + + object State_Init extends Notification0("PIDE/state_init") + object State_Exit extends State_Id_Notification("PIDE/state_exit") + object State_Locate extends State_Id_Notification("PIDE/state_locate") + object State_Update extends State_Id_Notification("PIDE/state_update") + + /* preview */ object Preview_Request