tuned;

--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue May 23 13:47:31 2017 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Tue May 23 14:23:26 2017 +0200
@@ -12,7 +12,7 @@
 
 object Dynamic_Output
 {
-  case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil)
+  sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil)
   {
     def handle_update(
       resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =