src/Pure/General/scan.scala

--- a/src/Pure/General/scan.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/scan.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.collection.generic.Addable
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
@@ -27,7 +28,7 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon extends scala.collection.Set[String] with RegexParsers
+  class Lexicon extends Addable[String, Lexicon] with RegexParsers
   {
     /* representation */
 
@@ -65,14 +66,14 @@
       }
 
 
-    /* Set methods */
+    /* pseudo Set methods */
 
-    override def stringPrefix = "Lexicon"
+    def iterator: Iterator[String] = content(main_tree, Nil).sort(_ <= _).iterator
 
-    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
+    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
 
-    def size: Int = content(main_tree, Nil).length
-    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
+    def empty: Lexicon = Lexicon.empty
+    def isEmpty: Boolean = main_tree.branches.isEmpty
 
     def contains(elem: String): Boolean =
       lookup(elem) match {
@@ -80,6 +81,11 @@
         case _ => false
       }
 
+
+    /* Addable methods */
+
+    def repr = this
+
     def + (elem: String): Lexicon =
       if (contains(elem)) this
       else {
@@ -102,11 +108,6 @@
         new Lexicon { override val main_tree = extend(old.main_tree, 0) }
       }
 
-    def + (elem1: String, elem2: String, elems: String*): Lexicon =
-      this + elem1 + elem2 ++ elems
-    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
-    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
-
 
 
     /** RegexParsers methods **/