--- 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] =
--- a/src/Pure/PIDE/command.scala Tue Jul 02 20:47:32 2013 +0200
+++ b/src/Pure/PIDE/command.scala Wed Jul 03 15:11:15 2013 +0200
@@ -227,7 +227,7 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- lazy val symbol_index = new Symbol.Index(source)
+ lazy val symbol_index = Symbol.Index(source)
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)