| changeset 70780 | 034742453594 |
| parent 70665 | 94442fce40a5 |
| child 71153 | 8563046f15c3 |
--- a/src/Pure/PIDE/markup.scala Tue Oct 01 20:21:30 2019 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Oct 02 14:45:37 2019 +0200 @@ -467,6 +467,7 @@ val CANCELED = "canceled" val INITIALIZED = "initialized" val FINALIZED = "finalized" + val CONSOLIDATING = "consolidating" val CONSOLIDATED = "consolidated"