src/Pure/PIDE/text.scala
changeset 56746 d37a5d09a277
parent 56590 d01d183e84ea
child 57620 c30ab960875e
     1.1 --- a/src/Pure/PIDE/text.scala	Sat Apr 26 13:32:28 2014 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Sat Apr 26 13:34:10 2014 +0200
     1.3 @@ -72,44 +72,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* named chunks with sparse symbol index */
     1.8 -
     1.9 -  object Chunk
    1.10 -  {
    1.11 -    sealed abstract class Name
    1.12 -    case object Default extends Name
    1.13 -    case class Id(id: Document_ID.Generic) extends Name
    1.14 -    case class File(name: String) extends Name
    1.15 -
    1.16 -    def apply(text: CharSequence): Chunk =
    1.17 -      new Chunk(Range(0, text.length), Symbol.Index(text))
    1.18 -  }
    1.19 -
    1.20 -  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
    1.21 -  {
    1.22 -    override def hashCode: Int = (range, symbol_index).hashCode
    1.23 -    override def equals(that: Any): Boolean =
    1.24 -      that match {
    1.25 -        case other: Chunk =>
    1.26 -          range == other.range &&
    1.27 -          symbol_index == other.symbol_index
    1.28 -        case _ => false
    1.29 -      }
    1.30 -
    1.31 -    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
    1.32 -    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
    1.33 -    def incorporate(symbol_range: Symbol.Range): Option[Range] =
    1.34 -    {
    1.35 -      def in(r: Symbol.Range): Option[Range] =
    1.36 -        range.try_restrict(decode(r)) match {
    1.37 -          case Some(r1) if !r1.is_singularity => Some(r1)
    1.38 -          case _ => None
    1.39 -        }
    1.40 -     in(symbol_range) orElse in(symbol_range - 1)
    1.41 -    }
    1.42 -  }
    1.43 -
    1.44 -
    1.45    /* perspective */
    1.46  
    1.47    object Perspective