1.1 --- a/src/Pure/General/scan.scala	Tue Jun 23 10:22:11 2009 +0200
     1.2 +++ b/src/Pure/General/scan.scala	Tue Jun 23 12:42:45 2009 +0200
     1.3 @@ -19,11 +19,8 @@
     1.4      private case class Tree(val branches: Map[Char, (String, Tree)])
     1.5      private val empty_tree = Tree(Map())
     1.6  
     1.7 -    private def make(tree: Tree): Lexicon =
     1.8 -      new Lexicon { override val main_tree = tree }
     1.9 -
    1.10      val empty: Lexicon = new Lexicon
    1.11 -    def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
    1.12 +    def apply(elems: String*): Lexicon = empty ++ elems
    1.13    }
    1.14  
    1.15    class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
    1.16 @@ -31,7 +28,7 @@
    1.17      /* representation */
    1.18  
    1.19      import Lexicon.Tree
    1.20 -    val main_tree: Tree = Lexicon.empty_tree
    1.21 +    private val main_tree: Tree = Lexicon.empty_tree
    1.22  
    1.23  
    1.24      /* auxiliary operations */
    1.25 @@ -75,34 +72,42 @@
    1.26      def size: Int = content(main_tree, Nil).length
    1.27      def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
    1.28  
    1.29 -    def contains(str: String): Boolean =
    1.30 -      lookup(str) match {
    1.31 +    def contains(elem: String): Boolean =
    1.32 +      lookup(elem) match {
    1.33          case Some((tip, _)) => tip
    1.34          case _ => false
    1.35        }
    1.36  
    1.37 -    def +(str: String): Lexicon =
    1.38 -    {
    1.39 -      val len = str.length
    1.40 -      def extend(tree: Tree, i: Int): Tree =
    1.41 -      {
    1.42 -        if (i < len) {
    1.43 -          val c = str.charAt(i)
    1.44 -          val end = (i + 1 == len)
    1.45 -          tree.branches.get(c) match {
    1.46 -            case Some((s, tr)) =>
    1.47 -              Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1))))
    1.48 -            case None =>
    1.49 -              Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1))))
    1.50 -          }
    1.51 -        } else tree
    1.52 +    def + (elem: String): Lexicon =
    1.53 +      if (contains(elem)) this
    1.54 +      else {
    1.55 +        val len = elem.length
    1.56 +        def extend(tree: Tree, i: Int): Tree =
    1.57 +          if (i < len) {
    1.58 +            val c = elem.charAt(i)
    1.59 +            val end = (i + 1 == len)
    1.60 +            tree.branches.get(c) match {
    1.61 +              case Some((s, tr)) =>
    1.62 +                Tree(tree.branches +
    1.63 +                  (c -> (if (end) elem else s, extend(tr, i + 1))))
    1.64 +              case None =>
    1.65 +                Tree(tree.branches +
    1.66 +                  (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1))))
    1.67 +            }
    1.68 +          } else tree
    1.69 +        val old = this
    1.70 +        new Lexicon { override val main_tree = extend(old.main_tree, 0) }
    1.71        }
    1.72 -      if (contains(str)) this
    1.73 -      else Lexicon.make(extend(main_tree, 0))
    1.74 -    }
    1.75 +
    1.76 +    override def + (elem1: String, elem2: String, elems: String*): Lexicon =
    1.77 +      this + elem1 + elem2 ++ elems
    1.78 +    override def ++ (elems: Iterable[String]): Lexicon =
    1.79 +      (this /: elems) ((s, elem) => s + elem)
    1.80 +    override def ++ (elems: Iterator[String]): Lexicon =
    1.81 +      (this /: elems) ((s, elem) => s + elem)
    1.82  
    1.83      def empty[A]: Set[A] = error("Undefined")
    1.84 -    def -(str: String): Lexicon = error("Undefined")
    1.85 +    def - (str: String): Lexicon = error("Undefined")
    1.86  
    1.87  
    1.88      /* RegexParsers methods */