src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -71,19 +71,25 @@
   }
 
 
-  /* chunks with symbol index */
+  /* named chunks with sparse symbol index */
 
-  abstract class Chunk
+  object Chunk
   {
-    def range: Range
-    def symbol_index: Symbol.Index
+    sealed abstract class Name
+    case object Default extends Name
+    case class Id(id: Document_ID.Generic) extends Name
+    case class File(name: String) extends Name
 
-    private lazy val hash: Int = (range, symbol_index).hashCode
-    override def hashCode: Int = hash
+    def apply(text: CharSequence): Chunk =
+      new Chunk(Range(0, text.length), Symbol.Index(text))
+  }
+
+  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
+  {
+    override def hashCode: Int = (range, symbol_index).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Chunk =>
-          hash == other.hash &&
           range == other.range &&
           symbol_index == other.symbol_index
         case _ => false
@@ -102,20 +108,6 @@
     }
   }
 
-  object Chunk
-  {
-    sealed abstract class Name
-    case object Default extends Name
-    case class Id(id: Document_ID.Generic) extends Name
-    case class File_Name(file_name: String) extends Name
-
-    class File(text: CharSequence) extends Chunk
-    {
-      val range = Range(0, text.length)
-      val symbol_index = Symbol.Index(text)
-    }
-  }
-
 
   /* perspective */