--- a/src/Pure/PIDE/markup.ML Fri Mar 21 16:42:20 2025 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Mar 21 18:37:05 2025 +0100
@@ -223,6 +223,7 @@
val consolidatingN: string val consolidating: T
val consolidatedN: string val consolidated: T
val exec_idN: string
+ val urgent_properties: Properties.T
val initN: string
val statusN: string val status: T
val resultN: string val result: T
@@ -752,6 +753,8 @@
val exec_idN = "exec_id";
+val urgent_properties = [("urgent", "true")];
+
val initN = "init";
val (statusN, status) = markup_elem "status";
val (resultN, result) = markup_elem "result";