src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Tue Apr 08 14:59:36 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 15:12:54 2014 +0200
@@ -71,6 +71,55 @@
   }
 
 
+  /* named chunks */
+
+  abstract class Chunk
+  {
+    def name: Chunk.Name
+    def range: Range
+    def symbol_index: Symbol.Index
+
+    private lazy val hash: Int = (name, range, symbol_index).hashCode
+    override def hashCode: Int = hash
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Chunk =>
+          hash == other.hash &&
+          name == other.name &&
+          range == other.range &&
+          symbol_index == other.symbol_index
+        case _ => false
+      }
+    override def toString: String = "Text.Chunk(" + name + ")"
+
+    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
+    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
+    def incorporate(symbol_range: Symbol.Range): Option[Range] =
+    {
+      def in(r: Symbol.Range): Option[Range] =
+        range.try_restrict(decode(r)) match {
+          case Some(r1) if !r1.is_singularity => Some(r1)
+          case _ => None
+        }
+     in(symbol_range) orElse in(symbol_range - 1)
+    }
+  }
+
+  object Chunk
+  {
+    sealed abstract class Name
+    case object Default extends Name
+    case class File_Name(file_name: String) extends Name
+
+    class File(file_name: String, text: CharSequence) extends Chunk
+    {
+      val name = File_Name(file_name)
+      val range = Range(0, text.length)
+      val symbol_index = Symbol.Index(text)
+    }
+  }
+
+
   /* perspective */
 
   object Perspective