diff -r f4abde849190 -r 5b5c750e9763 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 */