changeset 52507 | 27925b58d6bd |
parent 50564 | c6fde2fc4217 |
child 52616 | 3ac2878764f9 |
--- a/src/Pure/General/symbol.scala Tue Jul 02 20:47:32 2013 +0200 +++ b/src/Pure/General/symbol.scala Wed Jul 03 15:11:15 2013 +0200 @@ -111,7 +111,12 @@ /* decoding offsets */ - class Index(text: CharSequence) + object Index + { + def apply(text: CharSequence): Index = new Index(text) + } + + final class Index private(text: CharSequence) { sealed case class Entry(chr: Int, sym: Int) val index: Array[Entry] =