# HG changeset patch
# User wenzelm
# Date 1330026020 -3600
# Node ID fbe2cb05bdb39fce3018f739b1ec586ab508ec52
# Parent  a02115865bcc1b2dad00dcd2ef2ffb4ca44188a5
avoid trait Addable, which is deprecated in scala-2.9.x;
tuned;

diff -r a02115865bcc -r fbe2cb05bdb3 src/Pure/General/scan.scala
--- 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 **/