changeset 82316 | 83584916b6d7 |
parent 81346 | 0cdd6729a962 |
--- a/src/Pure/PIDE/protocol.scala Fri Mar 21 16:42:20 2025 +0100 +++ b/src/Pure/PIDE/protocol.scala Fri Mar 21 18:37:05 2025 +0100 @@ -107,6 +107,12 @@ /* result messages */ + def is_urgent(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(_, props), _) => Markup.Urgent.get(props) + case _ => false + } + def is_result(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.RESULT, _), _) => true