src/Pure/PIDE/protocol.scala

--- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:32:28 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:34:10 2014 +0200
@@ -312,8 +312,8 @@
 
   def message_positions(
     self_id: Document_ID.Generic => Boolean,
-    chunk_name: Text.Chunk.Name,
-    chunk: Text.Chunk,
+    chunk_name: Symbol.Text_Chunk.Name,
+    chunk: Symbol.Text_Chunk,
     message: XML.Elem): Set[Text.Range] =
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =