src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 06:43:06 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:07:20 2014 +0200
@@ -101,7 +101,7 @@
   }
 
   val proper_status_elements =
-    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
   val liberal_status_elements =
@@ -187,7 +187,7 @@
   /* result messages */
 
   private val clean_elements =
-    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
+    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
@@ -308,7 +308,7 @@
   /* reported positions */
 
   private val position_elements =
-    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,