tuned signature;
authorwenzelm
Tue, 11 Feb 2014 15:55:05 +0100
changeset 55430 8eb6c740ec1a
parent 55429 4a50f9e70dc1
child 55431 e0f20a44ff9d
tuned signature;
src/Pure/General/symbol.scala
src/Pure/PIDE/command.scala
--- 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)