tuned;
authorwenzelm
Tue Apr 08 20:00:53 2014 +0200 (2014-04-08)
changeset 56472f4abde849190
parent 56471 2293a4350716
child 56473 5b5c750e9763
tuned;
src/Pure/General/symbol.scala
     1.1 --- a/src/Pure/General/symbol.scala	Tue Apr 08 19:35:50 2014 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Apr 08 20:00:53 2014 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    {
     1.5      private sealed case class Entry(chr: Int, sym: Int)
     1.6  
     1.7 -    val empty: Index = new Index(Array())
     1.8 +    val empty: Index = new Index(Nil)
     1.9  
    1.10      def apply(text: CharSequence): Index =
    1.11      {
    1.12 @@ -141,12 +141,15 @@
    1.13          sym += 1
    1.14          if (n > 1) buf += Entry(chr, sym)
    1.15        }
    1.16 -      if (buf.isEmpty) empty else new Index(buf.toArray)
    1.17 +      if (buf.isEmpty) empty else new Index(buf.toList)
    1.18      }
    1.19    }
    1.20  
    1.21 -  final class Index private(private val index: Array[Index.Entry])
    1.22 +  final class Index private(entries: List[Index.Entry])
    1.23    {
    1.24 +    private val hash: Int = entries.hashCode
    1.25 +    private val index: Array[Index.Entry] = entries.toArray
    1.26 +
    1.27      def decode(symbol_offset: Offset): Text.Offset =
    1.28      {
    1.29        val sym = symbol_offset - 1
    1.30 @@ -167,7 +170,6 @@
    1.31      }
    1.32      def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
    1.33  
    1.34 -    private val hash: Int = index.toList.hashCode
    1.35      override def hashCode: Int = hash
    1.36      override def equals(that: Any): Boolean =
    1.37        that match {