src/Pure/PIDE/text.scala
changeset 56473 5b5c750e9763
parent 56470 8eda56033203
child 56590 d01d183e84ea
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 08 20:03:00 2014 +0200
     1.3 @@ -71,19 +71,25 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* chunks with symbol index */
     1.8 +  /* named chunks with sparse symbol index */
     1.9  
    1.10 -  abstract class Chunk
    1.11 +  object Chunk
    1.12    {
    1.13 -    def range: Range
    1.14 -    def symbol_index: Symbol.Index
    1.15 +    sealed abstract class Name
    1.16 +    case object Default extends Name
    1.17 +    case class Id(id: Document_ID.Generic) extends Name
    1.18 +    case class File(name: String) extends Name
    1.19  
    1.20 -    private lazy val hash: Int = (range, symbol_index).hashCode
    1.21 -    override def hashCode: Int = hash
    1.22 +    def apply(text: CharSequence): Chunk =
    1.23 +      new Chunk(Range(0, text.length), Symbol.Index(text))
    1.24 +  }
    1.25 +
    1.26 +  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
    1.27 +  {
    1.28 +    override def hashCode: Int = (range, symbol_index).hashCode
    1.29      override def equals(that: Any): Boolean =
    1.30        that match {
    1.31          case other: Chunk =>
    1.32 -          hash == other.hash &&
    1.33            range == other.range &&
    1.34            symbol_index == other.symbol_index
    1.35          case _ => false
    1.36 @@ -102,20 +108,6 @@
    1.37      }
    1.38    }
    1.39  
    1.40 -  object Chunk
    1.41 -  {
    1.42 -    sealed abstract class Name
    1.43 -    case object Default extends Name
    1.44 -    case class Id(id: Document_ID.Generic) extends Name
    1.45 -    case class File_Name(file_name: String) extends Name
    1.46 -
    1.47 -    class File(text: CharSequence) extends Chunk
    1.48 -    {
    1.49 -      val range = Range(0, text.length)
    1.50 -      val symbol_index = Symbol.Index(text)
    1.51 -    }
    1.52 -  }
    1.53 -
    1.54  
    1.55    /* perspective */
    1.56