src/Pure/General/symbol.scala
changeset 56338 f968f4e3d520
parent 56335 8953d4cc060a
child 56471 2293a4350716
equal deleted inserted replaced
56337:520148f9921d 56338:f968f4e3d520
   164       if (i < 0) sym
   164       if (i < 0) sym
   165       else index(i).chr + sym - index(i).sym
   165       else index(i).chr + sym - index(i).sym
   166     }
   166     }
   167     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
   167     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
   168 
   168 
   169     override def hashCode: Int = index.hashCode
   169     private val hash: Int = index.toList.hashCode
       
   170     override def hashCode: Int = hash
   170     override def equals(that: Any): Boolean =
   171     override def equals(that: Any): Boolean =
   171       that match {
   172       that match {
   172         case other: Index => index.sameElements(other.index)
   173         case other: Index => index.sameElements(other.index)
   173         case _ => false
   174         case _ => false
   174       }
   175       }