# HG changeset patch
# User wenzelm
# Date 1396980053 -7200
# Node ID f4abde849190e074111edc0ac6d6d60b3097a371
# Parent  2293a4350716fb054b9234e855c4f617e5dacbd5
tuned;

diff -r 2293a4350716 -r f4abde849190 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Apr 08 19:35:50 2014 +0200
+++ b/src/Pure/General/symbol.scala	Tue Apr 08 20:00:53 2014 +0200
@@ -127,7 +127,7 @@
   {
     private sealed case class Entry(chr: Int, sym: Int)
 
-    val empty: Index = new Index(Array())
+    val empty: Index = new Index(Nil)
 
     def apply(text: CharSequence): Index =
     {
@@ -141,12 +141,15 @@
         sym += 1
         if (n > 1) buf += Entry(chr, sym)
       }
-      if (buf.isEmpty) empty else new Index(buf.toArray)
+      if (buf.isEmpty) empty else new Index(buf.toList)
     }
   }
 
-  final class Index private(private val index: Array[Index.Entry])
+  final class Index private(entries: List[Index.Entry])
   {
+    private val hash: Int = entries.hashCode
+    private val index: Array[Index.Entry] = entries.toArray
+
     def decode(symbol_offset: Offset): Text.Offset =
     {
       val sym = symbol_offset - 1
@@ -167,7 +170,6 @@
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
 
-    private val hash: Int = index.toList.hashCode
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {