src/Pure/PIDE/protocol.scala

           case Markup.ACCEPTED => accepted = true
           case Markup.FORKED => touched = true; forks += 1
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
-          case Markup.WARNING => warned = true
+          case Markup.WARNING | Markup.LEGACY => warned = true
           case Markup.FAILED | Markup.ERROR => failed = true
           case _ =>
         }
       }
       Status(touched, accepted, warned, failed, forks, runs)

   val proper_status_elements =
     Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
   val liberal_status_elements =
-    proper_status_elements + Markup.WARNING + Markup.ERROR
+    proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
 
   /* command timing */
 
   object Command_Timing

       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
       case _ => false
     }
 
-  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
-    msg match {
-      case XML.Elem(Markup(Markup.WARNING, _),
-        List(XML.Elem(markup, _))) => markup.name == name
-      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
-        List(XML.Elem(markup, _))) => markup.name == name
-      case _ => false
-    }
-
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
+  def is_legacy(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.LEGACY, _), _) => true
+      case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
+      case _ => false
+    }
+
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.ERROR, _), _) => true
       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
-
-  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
 
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))