adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
authorwenzelm
Mon Mar 29 22:43:56 2010 +0200 (2010-03-29)
changeset 360113ff725ac13a4
parent 36010 a5e7574d8214
child 36012 0614676f14d4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
src/Pure/General/linear_set.scala
src/Pure/General/scan.scala
src/Pure/General/symbol.scala
src/Pure/General/xml.scala
src/Pure/System/isabelle_syntax.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/standard_system.scala
src/Pure/Thy/document.scala
src/Pure/Thy/html.scala
src/Pure/Thy/markup_node.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/linear_set.scala	Mon Mar 29 01:07:01 2010 -0700
     1.2 +++ b/src/Pure/General/linear_set.scala	Mon Mar 29 22:43:56 2010 +0200
     1.3 @@ -7,27 +7,36 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 +import scala.collection.SetLike
     1.8 +import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
     1.9  
    1.10 -object Linear_Set
    1.11 +
    1.12 +object Linear_Set extends SetFactory[Linear_Set]
    1.13  {
    1.14    private case class Rep[A](
    1.15 -    val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    1.16 +    val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    1.17  
    1.18    private def empty_rep[A] = Rep[A](None, None, Map(), Map())
    1.19  
    1.20 -  private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
    1.21 -    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
    1.22 +  private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
    1.23 +    : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
    1.24  
    1.25 -  def empty[A]: Linear_Set[A] = new Linear_Set
    1.26 -  def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
    1.27 +  implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
    1.28 +  override def empty[A] = new Linear_Set[A]
    1.29  
    1.30    class Duplicate(s: String) extends Exception(s)
    1.31    class Undefined(s: String) extends Exception(s)
    1.32  }
    1.33  
    1.34  
    1.35 -class Linear_Set[A] extends scala.collection.immutable.Set[A]
    1.36 +class Linear_Set[A]
    1.37 +  extends scala.collection.immutable.Set[A]
    1.38 +  with GenericSetTemplate[A, Linear_Set]
    1.39 +  with SetLike[A, Linear_Set[A]]
    1.40  {
    1.41 +  override def companion: GenericCompanion[Linear_Set] = Linear_Set
    1.42 +
    1.43 +
    1.44    /* representation */
    1.45  
    1.46    protected val rep = Linear_Set.empty_rep[A]
    1.47 @@ -43,10 +52,10 @@
    1.48      else
    1.49        hook match {
    1.50          case None =>
    1.51 -          rep.first match {
    1.52 +          rep.start match {
    1.53              case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
    1.54              case Some(elem1) =>
    1.55 -              Linear_Set.make(Some(elem), rep.last,
    1.56 +              Linear_Set.make(Some(elem), rep.end,
    1.57                  rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
    1.58            }
    1.59          case Some(elem1) =>
    1.60 @@ -54,10 +63,10 @@
    1.61            else
    1.62              rep.nexts.get(elem1) match {
    1.63                case None =>
    1.64 -                Linear_Set.make(rep.first, Some(elem),
    1.65 +                Linear_Set.make(rep.start, Some(elem),
    1.66                    rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
    1.67                case Some(elem2) =>
    1.68 -                Linear_Set.make(rep.first, rep.last,
    1.69 +                Linear_Set.make(rep.start, rep.end,
    1.70                    rep.nexts + (elem1 -> elem) + (elem -> elem2),
    1.71                    rep.prevs + (elem2 -> elem) + (elem -> elem1))
    1.72              }
    1.73 @@ -66,13 +75,13 @@
    1.74    def delete_after(hook: Option[A]): Linear_Set[A] =
    1.75      hook match {
    1.76        case None =>
    1.77 -        rep.first match {
    1.78 +        rep.start match {
    1.79            case None => throw new Linear_Set.Undefined("")
    1.80            case Some(elem1) =>
    1.81              rep.nexts.get(elem1) match {
    1.82                case None => empty
    1.83                case Some(elem2) =>
    1.84 -                Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
    1.85 +                Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
    1.86              }
    1.87          }
    1.88        case Some(elem1) =>
    1.89 @@ -83,9 +92,9 @@
    1.90              case Some(elem2) =>
    1.91                rep.nexts.get(elem2) match {
    1.92                  case None =>
    1.93 -                  Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
    1.94 +                  Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
    1.95                  case Some(elem3) =>
    1.96 -                  Linear_Set.make(rep.first, rep.last,
    1.97 +                  Linear_Set.make(rep.start, rep.end,
    1.98                      rep.nexts - elem2 + (elem1 -> elem3),
    1.99                      rep.prevs - elem2 + (elem3 -> elem1))
   1.100                }
   1.101 @@ -100,8 +109,8 @@
   1.102      if (isEmpty) this
   1.103      else {
   1.104        val next =
   1.105 -        if (from == rep.last) None
   1.106 -        else if (from == None) rep.first
   1.107 +        if (from == rep.end) None
   1.108 +        else if (from == None) rep.start
   1.109          else from.map(rep.nexts(_))
   1.110        if (next == to) this
   1.111        else delete_after(from).delete_between(from, to)
   1.112 @@ -113,15 +122,13 @@
   1.113  
   1.114    override def stringPrefix = "Linear_Set"
   1.115  
   1.116 -  def empty[B]: Linear_Set[B] = Linear_Set.empty
   1.117 -
   1.118 -  override def isEmpty: Boolean = !rep.first.isDefined
   1.119 -  def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   1.120 +  override def isEmpty: Boolean = !rep.start.isDefined
   1.121 +  override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
   1.122  
   1.123    def contains(elem: A): Boolean =
   1.124 -    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
   1.125 +    !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
   1.126  
   1.127 -  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
   1.128 +  private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
   1.129      private var next_elem = start
   1.130      def hasNext = next_elem.isDefined
   1.131      def next =
   1.132 @@ -133,18 +140,13 @@
   1.133        }
   1.134    }
   1.135  
   1.136 -  def elements: Iterator[A] = elements_from(rep.first)
   1.137 +  override def iterator: Iterator[A] = iterator_from(rep.start)
   1.138  
   1.139 -  def elements(elem: A): Iterator[A] =
   1.140 -    if (contains(elem)) elements_from(Some(elem))
   1.141 +  def iterator(elem: A): Iterator[A] =
   1.142 +    if (contains(elem)) iterator_from(Some(elem))
   1.143      else throw new Linear_Set.Undefined(elem.toString)
   1.144  
   1.145 -  def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
   1.146 -
   1.147 -  override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
   1.148 -    this + elem1 + elem2 ++ elems
   1.149 -  override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
   1.150 -  override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
   1.151 +  def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
   1.152  
   1.153    def - (elem: A): Linear_Set[A] =
   1.154      if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
     2.1 --- a/src/Pure/General/scan.scala	Mon Mar 29 01:07:01 2010 -0700
     2.2 +++ b/src/Pure/General/scan.scala	Mon Mar 29 22:43:56 2010 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.collection.generic.Addable
     2.8  import scala.collection.immutable.PagedSeq
     2.9  import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    2.10  import scala.util.parsing.combinator.RegexParsers
    2.11 @@ -27,7 +28,7 @@
    2.12      def apply(elems: String*): Lexicon = empty ++ elems
    2.13    }
    2.14  
    2.15 -  class Lexicon extends scala.collection.Set[String] with RegexParsers
    2.16 +  class Lexicon extends Addable[String, Lexicon] with RegexParsers
    2.17    {
    2.18      /* representation */
    2.19  
    2.20 @@ -65,14 +66,14 @@
    2.21        }
    2.22  
    2.23  
    2.24 -    /* Set methods */
    2.25 +    /* pseudo Set methods */
    2.26  
    2.27 -    override def stringPrefix = "Lexicon"
    2.28 +    def iterator: Iterator[String] = content(main_tree, Nil).sort(_ <= _).iterator
    2.29  
    2.30 -    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
    2.31 +    override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
    2.32  
    2.33 -    def size: Int = content(main_tree, Nil).length
    2.34 -    def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
    2.35 +    def empty: Lexicon = Lexicon.empty
    2.36 +    def isEmpty: Boolean = main_tree.branches.isEmpty
    2.37  
    2.38      def contains(elem: String): Boolean =
    2.39        lookup(elem) match {
    2.40 @@ -80,6 +81,11 @@
    2.41          case _ => false
    2.42        }
    2.43  
    2.44 +
    2.45 +    /* Addable methods */
    2.46 +
    2.47 +    def repr = this
    2.48 +
    2.49      def + (elem: String): Lexicon =
    2.50        if (contains(elem)) this
    2.51        else {
    2.52 @@ -102,11 +108,6 @@
    2.53          new Lexicon { override val main_tree = extend(old.main_tree, 0) }
    2.54        }
    2.55  
    2.56 -    def + (elem1: String, elem2: String, elems: String*): Lexicon =
    2.57 -      this + elem1 + elem2 ++ elems
    2.58 -    def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
    2.59 -    def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
    2.60 -
    2.61  
    2.62  
    2.63      /** RegexParsers methods **/
     3.1 --- a/src/Pure/General/symbol.scala	Mon Mar 29 01:07:01 2010 -0700
     3.2 +++ b/src/Pure/General/symbol.scala	Mon Mar 29 22:43:56 2010 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  package isabelle
     3.5  
     3.6  import scala.io.Source
     3.7 -import scala.collection.{jcl, mutable}
     3.8 +import scala.collection.mutable
     3.9  import scala.util.matching.Regex
    3.10  
    3.11  
    3.12 @@ -54,9 +54,9 @@
    3.13    }
    3.14  
    3.15  
    3.16 -  /* elements */
    3.17 +  /* iterator */
    3.18  
    3.19 -  def elements(text: CharSequence) = new Iterator[CharSequence]
    3.20 +  def iterator(text: CharSequence) = new Iterator[CharSequence]
    3.21    {
    3.22      private val matcher = new Matcher(text)
    3.23      private var i = 0
    3.24 @@ -124,12 +124,7 @@
    3.25        }
    3.26        (min, max)
    3.27      }
    3.28 -    private val table =
    3.29 -    {
    3.30 -      val table = new jcl.HashMap[String, String]   // reasonably efficient?
    3.31 -      for ((x, y) <- list) table + (x -> y)
    3.32 -      table
    3.33 -    }
    3.34 +    private val table = Map[String, String]() ++ list
    3.35      def recode(text: String): String =
    3.36      {
    3.37        val len = text.length
     4.1 --- a/src/Pure/General/xml.scala	Mon Mar 29 01:07:01 2010 -0700
     4.2 +++ b/src/Pure/General/xml.scala	Mon Mar 29 22:43:56 2010 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4    private def append_text(text: String, s: StringBuilder) {
     4.5      if (text == null) s ++ text
     4.6      else {
     4.7 -      for (c <- text.elements) c match {
     4.8 +      for (c <- text.iterator) c match {
     4.9          case '<' => s ++ "&lt;"
    4.10          case '>' => s ++ "&gt;"
    4.11          case '&' => s ++ "&amp;"
     5.1 --- a/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 01:07:01 2010 -0700
     5.2 +++ b/src/Pure/System/isabelle_syntax.scala	Mon Mar 29 22:43:56 2010 +0200
     5.3 @@ -40,7 +40,7 @@
     5.4      result: StringBuilder)
     5.5    {
     5.6      result.append("(")
     5.7 -    val elems = body.elements
     5.8 +    val elems = body.iterator
     5.9      if (elems.hasNext) append_elem(elems.next, result)
    5.10      while (elems.hasNext) {
    5.11        result.append(", ")
     6.1 --- a/src/Pure/System/isabelle_system.scala	Mon Mar 29 01:07:01 2010 -0700
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Mar 29 22:43:56 2010 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4  
     6.5    private val environment: Map[String, String] =
     6.6    {
     6.7 -    import scala.collection.jcl.Conversions._
     6.8 +    import scala.collection.JavaConversions._
     6.9  
    6.10      val env0 = Map(java.lang.System.getenv.toList: _*)
    6.11  
    6.12 @@ -297,7 +297,7 @@
    6.13    private def read_symbols(path: String): List[String] =
    6.14    {
    6.15      val file = platform_file(path)
    6.16 -    if (file.isFile) Source.fromFile(file).getLines.toList
    6.17 +    if (file.isFile) Source.fromFile(file).getLines().toList
    6.18      else Nil
    6.19    }
    6.20    val symbols = new Symbol.Interpretation(
     7.1 --- a/src/Pure/System/standard_system.scala	Mon Mar 29 01:07:01 2010 -0700
     7.2 +++ b/src/Pure/System/standard_system.scala	Mon Mar 29 22:43:56 2010 +0200
     7.3 @@ -12,7 +12,7 @@
     7.4    BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     7.5    File, FileFilter, IOException}
     7.6  
     7.7 -import scala.io.Source
     7.8 +import scala.io.{Source, Codec}
     7.9  import scala.util.matching.Regex
    7.10  import scala.collection.mutable
    7.11  
    7.12 @@ -20,6 +20,7 @@
    7.13  object Standard_System
    7.14  {
    7.15    val charset = "UTF-8"
    7.16 +  val codec = Codec(charset)
    7.17  
    7.18  
    7.19    /* permissive UTF-8 decoding */
    7.20 @@ -135,7 +136,7 @@
    7.21    def process_output(proc: Process): (String, Int) =
    7.22    {
    7.23      proc.getOutputStream.close
    7.24 -    val output = Source.fromInputStream(proc.getInputStream, charset).mkString  // FIXME
    7.25 +    val output = Source.fromInputStream(proc.getInputStream)(codec).mkString  // FIXME
    7.26      val rc =
    7.27        try { proc.waitFor }
    7.28        finally {
     8.1 --- a/src/Pure/Thy/document.scala	Mon Mar 29 01:07:01 2010 -0700
     8.2 +++ b/src/Pure/Thy/document.scala	Mon Mar 29 22:43:56 2010 +0200
     8.3 @@ -14,7 +14,7 @@
     8.4    def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
     8.5    {
     8.6      var offset = 0
     8.7 -    for (cmd <- commands.elements) yield {
     8.8 +    for (cmd <- commands.iterator) yield {
     8.9        val start = offset
    8.10        offset += cmd.length
    8.11        (cmd, start)
    8.12 @@ -92,10 +92,10 @@
    8.13      def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    8.14      {
    8.15        // FIXME relative search!
    8.16 -      commands.elements.find(is_unparsed) match {
    8.17 +      commands.iterator.find(is_unparsed) match {
    8.18          case Some(first_unparsed) =>
    8.19            val prefix = commands.prev(first_unparsed)
    8.20 -          val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
    8.21 +          val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
    8.22            val suffix = commands.next(body.last)
    8.23  
    8.24            val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
    8.25 @@ -128,8 +128,8 @@
    8.26        val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
    8.27        val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
    8.28  
    8.29 -      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
    8.30 -      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
    8.31 +      val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    8.32 +      val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    8.33  
    8.34        val doc_edits =
    8.35          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
     9.1 --- a/src/Pure/Thy/html.scala	Mon Mar 29 01:07:01 2010 -0700
     9.2 +++ b/src/Pure/Thy/html.scala	Mon Mar 29 22:43:56 2010 +0200
     9.3 @@ -49,7 +49,7 @@
     9.4            flush()
     9.5            ts + elem
     9.6          }
     9.7 -        val syms = Symbol.elements(txt).map(_.toString)
     9.8 +        val syms = Symbol.iterator(txt).map(_.toString)
     9.9          while (syms.hasNext) {
    9.10            val s1 = syms.next
    9.11            def s2() = if (syms.hasNext) syms.next else ""
    10.1 --- a/src/Pure/Thy/markup_node.scala	Mon Mar 29 01:07:01 2010 -0700
    10.2 +++ b/src/Pure/Thy/markup_node.scala	Mon Mar 29 22:43:56 2010 +0200
    10.3 @@ -70,7 +70,7 @@
    10.4            markup <- markups
    10.5          } yield markup
    10.6        if (next_x < node.stop)
    10.7 -        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
    10.8 +        filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
    10.9        else filled_gaps
   10.10      }
   10.11    }
    11.1 --- a/src/Pure/build-jars	Mon Mar 29 01:07:01 2010 -0700
    11.2 +++ b/src/Pure/build-jars	Mon Mar 29 22:43:56 2010 +0200
    11.3 @@ -88,7 +88,7 @@
    11.4    echo "###"
    11.5  
    11.6    rm -rf classes && mkdir classes
    11.7 -  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \
    11.8 +  "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
    11.9      fail "Failed to compile sources"
   11.10    mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
   11.11    (