--- a/src/Pure/PIDE/markup.ML Tue Oct 01 20:21:30 2019 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Oct 02 14:45:37 2019 +0200
@@ -182,6 +182,7 @@
val canceledN: string val canceled: T
val initializedN: string val initialized: T
val finalizedN: string val finalized: T
+ val consolidatingN: string val consolidating: T
val consolidatedN: string val consolidated: T
val exec_idN: string
val initN: string
@@ -631,6 +632,7 @@
val (canceledN, canceled) = markup_elem "canceled";
val (initializedN, initialized) = markup_elem "initialized";
val (finalizedN, finalized) = markup_elem "finalized";
+val (consolidatingN, consolidating) = markup_elem "consolidating";
val (consolidatedN, consolidated) = markup_elem "consolidated";