# HG changeset patch
# User wenzelm
# Date 1269895436 -7200
# Node ID 3ff725ac13a48f20d08066c0ec80a4dcd06ca677
# Parent  a5e7574d8214aa92308551134de90d2f2a9fd1ec
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;

diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/linear_set.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -7,27 +7,36 @@
 
 package isabelle
 
+import scala.collection.SetLike
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
 
-object Linear_Set
+
+object Linear_Set extends SetFactory[Linear_Set]
 {
   private case class Rep[A](
-    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
+    val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
 
   private def empty_rep[A] = Rep[A](None, None, Map(), Map())
 
-  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
-    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
+  private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
 
-  def empty[A]: Linear_Set[A] = new Linear_Set
-  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+  implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+  override def empty[A] = new Linear_Set[A]
 
   class Duplicate(s: String) extends Exception(s)
   class Undefined(s: String) extends Exception(s)
 }
 
 
-class Linear_Set[A] extends scala.collection.immutable.Set[A]
+class Linear_Set[A]
+  extends scala.collection.immutable.Set[A]
+  with GenericSetTemplate[A, Linear_Set]
+  with SetLike[A, Linear_Set[A]]
 {
+  override def companion: GenericCompanion[Linear_Set] = Linear_Set
+
+
   /* representation */
 
   protected val rep = Linear_Set.empty_rep[A]
@@ -43,10 +52,10 @@
     else
       hook match {
         case None =>
-          rep.first match {
+          rep.start match {
             case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
             case Some(elem1) =>
-              Linear_Set.make(Some(elem), rep.last,
+              Linear_Set.make(Some(elem), rep.end,
                 rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
           }
         case Some(elem1) =>
@@ -54,10 +63,10 @@
           else
             rep.nexts.get(elem1) match {
               case None =>
-                Linear_Set.make(rep.first, Some(elem),
+                Linear_Set.make(rep.start, Some(elem),
                   rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
               case Some(elem2) =>
-                Linear_Set.make(rep.first, rep.last,
+                Linear_Set.make(rep.start, rep.end,
                   rep.nexts + (elem1 -> elem) + (elem -> elem2),
                   rep.prevs + (elem2 -> elem) + (elem -> elem1))
             }
@@ -66,13 +75,13 @@
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
-        rep.first match {
+        rep.start match {
           case None => throw new Linear_Set.Undefined("")
           case Some(elem1) =>
             rep.nexts.get(elem1) match {
               case None => empty
               case Some(elem2) =>
-                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+                Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
             }
         }
       case Some(elem1) =>
@@ -83,9 +92,9 @@
             case Some(elem2) =>
               rep.nexts.get(elem2) match {
                 case None =>
-                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+                  Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
                 case Some(elem3) =>
-                  Linear_Set.make(rep.first, rep.last,
+                  Linear_Set.make(rep.start, rep.end,
                     rep.nexts - elem2 + (elem1 -> elem3),
                     rep.prevs - elem2 + (elem3 -> elem1))
               }
@@ -100,8 +109,8 @@
     if (isEmpty) this
     else {
       val next =
-        if (from == rep.last) None
-        else if (from == None) rep.first
+        if (from == rep.end) None
+        else if (from == None) rep.start
         else from.map(rep.nexts(_))
       if (next == to) this
       else delete_after(from).delete_between(from, to)
@@ -113,15 +122,13 @@
 
   override def stringPrefix = "Linear_Set"
 
-  def empty[B]: Linear_Set[B] = Linear_Set.empty
-
-  override def isEmpty: Boolean = !rep.first.isDefined
-  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+  override def isEmpty: Boolean = !rep.start.isDefined
+  override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
   def contains(elem: A): Boolean =
-    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+    !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
 
-  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+  private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
     def hasNext = next_elem.isDefined
     def next =
@@ -133,18 +140,13 @@
       }
   }
 
-  def elements: Iterator[A] = elements_from(rep.first)
+  override def iterator: Iterator[A] = iterator_from(rep.start)
 
-  def elements(elem: A): Iterator[A] =
-    if (contains(elem)) elements_from(Some(elem))
+  def iterator(elem: A): Iterator[A] =
+    if (contains(elem)) iterator_from(Some(elem))
     else throw new Linear_Set.Undefined(elem.toString)
 
-  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
-
-  override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
-    this + elem1 + elem2 ++ elems
-  override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
-  override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+  def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
 
   def - (elem: A): Linear_Set[A] =
     if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
diff -r a5e7574d8214 -r 3ff725ac13a4 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 **/
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/symbol.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 import scala.io.Source
-import scala.collection.{jcl, mutable}
+import scala.collection.mutable
 import scala.util.matching.Regex
 
 
@@ -54,9 +54,9 @@
   }
 
 
-  /* elements */
+  /* iterator */
 
-  def elements(text: CharSequence) = new Iterator[CharSequence]
+  def iterator(text: CharSequence) = new Iterator[CharSequence]
   {
     private val matcher = new Matcher(text)
     private var i = 0
@@ -124,12 +124,7 @@
       }
       (min, max)
     }
-    private val table =
-    {
-      val table = new jcl.HashMap[String, String]   // reasonably efficient?
-      for ((x, y) <- list) table + (x -> y)
-      table
-    }
+    private val table = Map[String, String]() ++ list
     def recode(text: String): String =
     {
       val len = text.length
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/General/xml.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -36,7 +36,7 @@
   private def append_text(text: String, s: StringBuilder) {
     if (text == null) s ++ text
     else {
-      for (c <- text.elements) c match {
+      for (c <- text.iterator) c match {
         case '<' => s ++ "&lt;"
         case '>' => s ++ "&gt;"
         case '&' => s ++ "&amp;"
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/System/isabelle_syntax.scala
--- a/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -40,7 +40,7 @@
     result: StringBuilder)
   {
     result.append("(")
-    val elems = body.elements
+    val elems = body.iterator
     if (elems.hasNext) append_elem(elems.next, result)
     while (elems.hasNext) {
       result.append(", ")
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/System/isabelle_system.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -24,7 +24,7 @@
 
   private val environment: Map[String, String] =
   {
-    import scala.collection.jcl.Conversions._
+    import scala.collection.JavaConversions._
 
     val env0 = Map(java.lang.System.getenv.toList: _*)
 
@@ -297,7 +297,7 @@
   private def read_symbols(path: String): List[String] =
   {
     val file = platform_file(path)
-    if (file.isFile) Source.fromFile(file).getLines.toList
+    if (file.isFile) Source.fromFile(file).getLines().toList
     else Nil
   }
   val symbols = new Symbol.Interpretation(
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/System/standard_system.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -12,7 +12,7 @@
   BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
 
-import scala.io.Source
+import scala.io.{Source, Codec}
 import scala.util.matching.Regex
 import scala.collection.mutable
 
@@ -20,6 +20,7 @@
 object Standard_System
 {
   val charset = "UTF-8"
+  val codec = Codec(charset)
 
 
   /* permissive UTF-8 decoding */
@@ -135,7 +136,7 @@
   def process_output(proc: Process): (String, Int) =
   {
     proc.getOutputStream.close
-    val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
+    val output = Source.fromInputStream(proc.getInputStream)(codec).mkString  // FIXME
     val rc =
       try { proc.waitFor }
       finally {
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/Thy/document.scala
--- a/src/Pure/Thy/document.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/Thy/document.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -14,7 +14,7 @@
   def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
   {
     var offset = 0
-    for (cmd <- commands.elements) yield {
+    for (cmd <- commands.iterator) yield {
       val start = offset
       offset += cmd.length
       (cmd, start)
@@ -92,10 +92,10 @@
     def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
     {
       // FIXME relative search!
-      commands.elements.find(is_unparsed) match {
+      commands.iterator.find(is_unparsed) match {
         case Some(first_unparsed) =>
           val prefix = commands.prev(first_unparsed)
-          val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
+          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
           val suffix = commands.next(body.last)
 
           val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
@@ -128,8 +128,8 @@
       val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
       val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
 
-      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
-      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
 
       val doc_edits =
         removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -49,7 +49,7 @@
           flush()
           ts + elem
         }
-        val syms = Symbol.elements(txt).map(_.toString)
+        val syms = Symbol.iterator(txt).map(_.toString)
         while (syms.hasNext) {
           val s1 = syms.next
           def s2() = if (syms.hasNext) syms.next else ""
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/Thy/markup_node.scala
--- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/Thy/markup_node.scala	Mon Mar 29 22:43:56 2010 +0200
@@ -70,7 +70,7 @@
           markup <- markups
         } yield markup
       if (next_x < node.stop)
-        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
       else filled_gaps
     }
   }
diff -r a5e7574d8214 -r 3ff725ac13a4 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Mar 29 01:07:01 2010 -0700
+++ b/src/Pure/build-jars	Mon Mar 29 22:43:56 2010 +0200
@@ -88,7 +88,7 @@
   echo "###"
 
   rm -rf classes && mkdir classes
-  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \
+  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
     fail "Failed to compile sources"
   mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
   (