# 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