# HG changeset patch
# User wenzelm
# Date 1245753765 -7200
# Node ID 20745ab5b79a18fa4a9caaad296b7f54fb448e95
# Parent  3585bebe49a87887a08b7d28185006423bd5b002
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
misc tuning;

diff -r 3585bebe49a8 -r 20745ab5b79a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Jun 23 10:22:11 2009 +0200
+++ b/src/Pure/General/scan.scala	Tue Jun 23 12:42:45 2009 +0200
@@ -19,11 +19,8 @@
     private case class Tree(val branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
-    private def make(tree: Tree): Lexicon =
-      new Lexicon { override val main_tree = tree }
-
     val empty: Lexicon = new Lexicon
-    def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
+    def apply(elems: String*): Lexicon = empty ++ elems
   }
 
   class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
@@ -31,7 +28,7 @@
     /* representation */
 
     import Lexicon.Tree
-    val main_tree: Tree = Lexicon.empty_tree
+    private val main_tree: Tree = Lexicon.empty_tree
 
 
     /* auxiliary operations */
@@ -75,34 +72,42 @@
     def size: Int = content(main_tree, Nil).length
     def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
 
-    def contains(str: String): Boolean =
-      lookup(str) match {
+    def contains(elem: String): Boolean =
+      lookup(elem) match {
         case Some((tip, _)) => tip
         case _ => false
       }
 
-    def +(str: String): Lexicon =
-    {
-      val len = str.length
-      def extend(tree: Tree, i: Int): Tree =
-      {
-        if (i < len) {
-          val c = str.charAt(i)
-          val end = (i + 1 == len)
-          tree.branches.get(c) match {
-            case Some((s, tr)) =>
-              Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1))))
-            case None =>
-              Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1))))
-          }
-        } else tree
+    def + (elem: String): Lexicon =
+      if (contains(elem)) this
+      else {
+        val len = elem.length
+        def extend(tree: Tree, i: Int): Tree =
+          if (i < len) {
+            val c = elem.charAt(i)
+            val end = (i + 1 == len)
+            tree.branches.get(c) match {
+              case Some((s, tr)) =>
+                Tree(tree.branches +
+                  (c -> (if (end) elem else s, extend(tr, i + 1))))
+              case None =>
+                Tree(tree.branches +
+                  (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
+            }
+          } else tree
+        val old = this
+        new Lexicon { override val main_tree = extend(old.main_tree, 0) }
       }
-      if (contains(str)) this
-      else Lexicon.make(extend(main_tree, 0))
-    }
+
+    override 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 - (str: String): Lexicon = error("Undefined")
 
 
     /* RegexParsers methods */