--- a/src/Pure/General/symbol.scala Tue Feb 11 15:05:13 2014 +0100
+++ b/src/Pure/General/symbol.scala Tue Feb 11 15:55:05 2014 +0100
@@ -118,8 +118,8 @@
final class Index private(text: CharSequence)
{
- sealed case class Entry(chr: Int, sym: Int)
- val index: Array[Entry] =
+ private sealed case class Entry(chr: Int, sym: Int)
+ private val index: Array[Entry] =
{
val matcher = new Matcher(text)
val buf = new mutable.ArrayBuffer[Entry]
@@ -133,6 +133,7 @@
}
buf.toArray
}
+
def decode(sym1: Int): Int =
{
val sym = sym1 - 1
--- a/src/Pure/PIDE/command.scala Tue Feb 11 15:05:13 2014 +0100
+++ b/src/Pure/PIDE/command.scala Tue Feb 11 15:55:05 2014 +0100
@@ -256,7 +256,7 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- lazy val symbol_index = Symbol.Index(source)
+ private 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)