# HG changeset patch
# User wenzelm
# Date 1392130505 -3600
# Node ID 8eb6c740ec1abc0f4ee99af6441f41690806779e
# Parent  4a50f9e70dc12e93b550319bce545e1fcc494233
tuned signature;

diff -r 4a50f9e70dc1 -r 8eb6c740ec1a src/Pure/General/symbol.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
diff -r 4a50f9e70dc1 -r 8eb6c740ec1a src/Pure/PIDE/command.scala
--- 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)