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" }