changeset 39622 | 53365ba766ac |
parent 39511 | 5f318522e6fe |
child 39625 | fb0c851e4f9d |
--- a/src/Pure/PIDE/isar_document.scala Wed Sep 22 22:25:21 2010 +0200 +++ b/src/Pure/PIDE/isar_document.scala Wed Sep 22 22:39:17 2010 +0200 @@ -72,6 +72,12 @@ /* specific messages */ + def is_tracing(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Markup.TRACING, _), _) => true + case _ => false + } + def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true