diff -r 6c68eff8355a -r 83584916b6d7 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Mar 21 16:42:20 2025 +0100 +++ b/src/Pure/PIDE/markup.scala Fri Mar 21 18:37:05 2025 +0100 @@ -584,6 +584,8 @@ /* messages */ + val Urgent = new Properties.Boolean("urgent") + val INIT = "init" val STATUS = "status" val REPORT = "report"