src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Sat Mar 01 09:34:08 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Mar 01 12:07:26 2014 +0100
@@ -77,11 +77,11 @@
   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
 
 
@@ -165,7 +165,8 @@
 
   /* 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 {
@@ -276,7 +277,7 @@
   /* 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,