# HG changeset patch
# User wenzelm
# Date 1372857075 -7200
# Node ID 27925b58d6bdf67b95d462b92b932c03deb963f9
# Parent  750b63fa4c4e87544ba044d1d633a642a0125533
tuned signature;

diff -r 750b63fa4c4e -r 27925b58d6bd src/Pure/General/symbol.scala
--- 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] =
diff -r 750b63fa4c4e -r 27925b58d6bd src/Pure/PIDE/command.scala
--- 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)