--- a/src/Pure/General/scan.scala Thu Feb 23 20:24:05 2012 +0100
+++ b/src/Pure/General/scan.scala Thu Feb 23 20:40:20 2012 +0100
@@ -7,8 +7,7 @@
package isabelle
-import scala.collection.generic.Addable
-import scala.collection.IndexedSeq
+import scala.collection.{IndexedSeq, TraversableOnce}
import scala.collection.immutable.PagedSeq
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
import scala.util.parsing.combinator.RegexParsers
@@ -41,8 +40,7 @@
def apply(elems: String*): Lexicon = empty ++ elems
}
- class Lexicon private(private val main_tree: Lexicon.Tree)
- extends Addable[String, Lexicon] with RegexParsers
+ class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
{
import Lexicon.Tree
@@ -93,9 +91,7 @@
}
- /* Addable methods */
-
- def repr = this
+ /* add elements */
def + (elem: String): Lexicon =
if (contains(elem)) this
@@ -115,10 +111,11 @@
}
}
else tree
- val old = this
- new Lexicon(extend(old.main_tree, 0))
+ new Lexicon(extend(main_tree, 0))
}
+ def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _)
+
/** RegexParsers methods **/