src/Pure/PIDE/markup.scala
changeset 68770 add44e2b8cb0
parent 68323 bf7336731981
child 68822 253f04c1e814
     1.1 --- a/src/Pure/PIDE/markup.scala	Sat Aug 18 17:29:49 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Sat Aug 18 22:09:09 2018 +0200
     1.3 @@ -456,6 +456,7 @@
     1.4    val WARNING = "warning"
     1.5    val LEGACY = "legacy"
     1.6    val ERROR = "error"
     1.7 +  val NODES_STATUS = "nodes_status"
     1.8    val PROTOCOL = "protocol"
     1.9    val SYSTEM = "system"
    1.10    val STDOUT = "stdout"