# HG changeset patch # User wenzelm # Date 1396978550 -7200 # Node ID 2293a4350716fb054b9234e855c4f617e5dacbd5 # Parent 8eda560332036cb9c1c5842b638244368fe4f859 more frugal Symbol.Index -- no need to waste space on mostly empty arrays; diff -r 8eda56033203 -r 2293a4350716 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Tue Apr 08 19:17:28 2014 +0200 +++ b/src/Pure/General/symbol.scala Tue Apr 08 19:35:50 2014 +0200 @@ -125,16 +125,14 @@ object Index { - def apply(text: CharSequence): Index = new Index(text) - } + private sealed case class Entry(chr: Int, sym: Int) - final class Index private(text: CharSequence) - { - private sealed case class Entry(chr: Int, sym: Int) - private val index: Array[Entry] = + val empty: Index = new Index(Array()) + + def apply(text: CharSequence): Index = { val matcher = new Matcher(text) - val buf = new mutable.ArrayBuffer[Entry] + val buf = new mutable.ListBuffer[Entry] var chr = 0 var sym = 0 while (chr < text.length) { @@ -143,9 +141,12 @@ sym += 1 if (n > 1) buf += Entry(chr, sym) } - buf.toArray + if (buf.isEmpty) empty else new Index(buf.toArray) } + } + final class Index private(private val index: Array[Index.Entry]) + { def decode(symbol_offset: Offset): Text.Offset = { val sym = symbol_offset - 1