src/Pure/PIDE/protocol.scala

     }
 
   def command_status(markups: List[Markup]): Status =
     (Status.init /: markups)(command_status(_, _))
 
-  val command_status_elements: Set[String] =
-    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+  val command_status_elements =
+    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
-  val status_elements: Set[String] =
+  val status_elements =
     command_status_elements + Markup.WARNING + Markup.ERROR
 
 
   /* command timing */
 

   }
 
 
   /* result messages */
 
-  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
+  private val clean_elements =
+    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
       case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
       case XML.Elem(Markup(name, _), _) => !clean_elements(name)

 
 
   /* reported positions */
 
   private val position_elements =
-    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     command_id: Document_ID.Command,
     alt_id: Document_ID.Generic,
     chunk: Command.Chunk,