# HG changeset patch
# User wenzelm
# Date 1495542206 -7200
# Node ID f9c2770a9c561bf0d6e0c14b3d2b0d27897b5ce0
# Parent  f97d163479b9ff26fe293ddebaf9ef5cec9ab359
tuned;

diff -r f97d163479b9 -r f9c2770a9c56 src/Tools/VSCode/src/dynamic_output.scala
--- 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 =