src/Pure/General/scan.scala

--- a/src/Pure/General/scan.scala	Tue Jun 23 17:43:23 2009 +0200
+++ b/src/Pure/General/scan.scala	Tue Jun 23 17:43:51 2009 +0200
@@ -23,12 +23,12 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
+  class Lexicon extends scala.collection.Set[String] with RegexParsers
   {
     /* representation */
 
     import Lexicon.Tree
-    private val main_tree: Tree = Lexicon.empty_tree
+    protected val main_tree: Tree = Lexicon.empty_tree
 
 
     /* auxiliary operations */
@@ -54,13 +54,11 @@
     }
 
     def completions(str: CharSequence): List[String] =
-    {
-      (lookup(str) match {
+      lookup(str) match {
         case Some((true, tree)) => content(tree, List(str.toString))
         case Some((false, tree)) => content(tree, Nil)
         case None => Nil
-      }).sort((s1, s2) => s1.length < s2.length || s1.length == s2.length && s1 <= s2)
-    }
+      }
 
 
     /* Set methods */
@@ -99,15 +97,10 @@
         new Lexicon { override val main_tree = extend(old.main_tree, 0) }
       }
 
-    override def + (elem1: String, elem2: String, elems: String*): Lexicon =
+    def + (elem1: String, elem2: String, elems: String*): Lexicon =
       this + elem1 + elem2 ++ elems
-    override def ++ (elems: Iterable[String]): Lexicon =
-      (this /: elems) ((s, elem) => s + elem)
-    override def ++ (elems: Iterator[String]): Lexicon =
-      (this /: elems) ((s, elem) => s + elem)
-
-    def empty[A]: Set[A] = error("Undefined")
-    def - (str: String): Lexicon = error("Undefined")
+    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
+    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
 
 
     /* RegexParsers methods */
@@ -137,31 +130,5 @@
     }.named("keyword")
 
   }
-
-
-  /** reverse CharSequence **/
-
-  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
-  {
-    require(0 <= start && start <= end && end <= text.length)
-
-    def this(text: CharSequence) = this(text, 0, text.length)
-
-    def length: Int = end - start
-    def charAt(i: Int): Char = text.charAt(end - i - 1)
-
-    def subSequence(i: Int, j: Int): CharSequence =
-      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
-      else throw new IndexOutOfBoundsException
-
-    override def toString: String =
-    {
-      val buf = new StringBuffer(length)
-      for (i <- 0 until length)
-        buf.append(charAt(i))
-      buf.toString
-    }
-  }
-
 }