src/Pure/PIDE/protocol.scala
changeset 72878 80465b791f95
parent 72877 313c281766cd
child 72946 9329abcdd651
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 10 21:48:53 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Dec 10 22:15:16 2020 +0100
@@ -191,6 +191,7 @@
           else if (is_error(elem)) "Error"
           else if (is_information(elem)) "Information"
           else if (is_tracing(elem)) "Tracing"
+          else if (is_state(elem)) "State"
           else "Output"
         "\n" + h + Position.here(pos) + ":\n"
       }