src/Pure/General/scan.scala
changeset 59073 dcecfcc56dce
parent 58505 d1fe47fe5401
child 59319 677615cba30d
     1.1 --- a/src/Pure/General/scan.scala	Mon Dec 01 14:24:05 2014 +0100
     1.2 +++ b/src/Pure/General/scan.scala	Mon Dec 01 15:21:49 2014 +0100
     1.3 @@ -318,10 +318,10 @@
     1.4    {
     1.5      /* auxiliary operations */
     1.6  
     1.7 -    private def content(tree: Lexicon.Tree, result: List[String]): List[String] =
     1.8 +    private def dest(tree: Lexicon.Tree, result: List[String]): List[String] =
     1.9        (result /: tree.branches.toList) ((res, entry) =>
    1.10          entry match { case (_, (s, tr)) =>
    1.11 -          if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
    1.12 +          if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) })
    1.13  
    1.14      private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] =
    1.15      {
    1.16 @@ -341,20 +341,20 @@
    1.17  
    1.18      def completions(str: CharSequence): List[String] =
    1.19        lookup(str) match {
    1.20 -        case Some((true, tree)) => content(tree, List(str.toString))
    1.21 -        case Some((false, tree)) => content(tree, Nil)
    1.22 +        case Some((true, tree)) => dest(tree, List(str.toString))
    1.23 +        case Some((false, tree)) => dest(tree, Nil)
    1.24          case None => Nil
    1.25        }
    1.26  
    1.27  
    1.28      /* pseudo Set methods */
    1.29  
    1.30 -    def iterator: Iterator[String] = content(rep, Nil).sorted.iterator
    1.31 +    def raw_iterator: Iterator[String] = dest(rep, Nil).iterator
    1.32 +    def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator
    1.33  
    1.34      override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    1.35  
    1.36 -    def empty: Lexicon = Lexicon.empty
    1.37 -    def isEmpty: Boolean = rep.branches.isEmpty
    1.38 +    def is_empty: Boolean = rep.branches.isEmpty
    1.39  
    1.40      def contains(elem: String): Boolean =
    1.41        lookup(elem) match {
    1.42 @@ -363,7 +363,7 @@
    1.43        }
    1.44  
    1.45  
    1.46 -    /* add elements */
    1.47 +    /* build lexicon */
    1.48  
    1.49      def + (elem: String): Lexicon =
    1.50        if (contains(elem)) this
    1.51 @@ -388,6 +388,11 @@
    1.52  
    1.53      def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
    1.54  
    1.55 +    def ++ (other: Lexicon): Lexicon =
    1.56 +      if (this eq other) this
    1.57 +      else if (is_empty) other
    1.58 +      else this ++ other.raw_iterator
    1.59 +
    1.60  
    1.61      /* scan */
    1.62