src/Pure/General/symbol.scala
changeset 56335 8953d4cc060a
parent 55884 f2c0eaedd579
child 56338 f968f4e3d520
equal deleted inserted replaced
56334:6b3739fee456 56335:8953d4cc060a
   163       val i = bisect(0, end)
   163       val i = bisect(0, end)
   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 
       
   169     override def hashCode: Int = index.hashCode
       
   170     override def equals(that: Any): Boolean =
       
   171       that match {
       
   172         case other: Index => index.sameElements(other.index)
       
   173         case _ => false
       
   174       }
   168   }
   175   }
   169 
   176 
   170 
   177 
   171   /* recoding text */
   178   /* recoding text */
   172 
   179