diff -r 313c281766cd -r 80465b791f95 src/Pure/PIDE/protocol.scala --- 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" }