--- a/Admin/components/components.sha1 Sat Jan 16 19:25:20 2021 +0100
+++ b/Admin/components/components.sha1 Sat Jan 16 22:52:43 2021 +0100
@@ -311,6 +311,7 @@
54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz
02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
+ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Sat Jan 16 19:25:20 2021 +0100
+++ b/Admin/components/main Sat Jan 16 22:52:43 2021 +0100
@@ -15,7 +15,7 @@
opam-2.0.7
polyml-test-f86ae3dc1686
postgresql-42.2.18
-scala-2.12.12
+scala-2.13.4
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.34.0
--- a/etc/settings Sat Jan 16 19:25:20 2021 +0100
+++ b/etc/settings Sat Jan 16 22:52:43 2021 +0100
@@ -16,7 +16,7 @@
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -J-Xms512m -J-Xmx4g -J-Xss16m"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/src/Pure/General/linear_set.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/General/linear_set.scala Sat Jan 16 22:52:43 2021 +0100
@@ -8,19 +8,26 @@
package isabelle
-import scala.collection.SetLike
-import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
-import scala.collection.mutable.{Builder, SetBuilder}
-import scala.language.higherKinds
+import scala.collection.mutable
+import scala.collection.immutable.SetOps
+import scala.collection.{IterableFactory, IterableFactoryDefaults}
-object Linear_Set extends SetFactory[Linear_Set]
+object Linear_Set extends IterableFactory[Linear_Set]
{
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
- implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
- def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
+ def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_))
+
+ override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
+ private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]
+ {
+ private var res = empty[A]
+ override def clear() { res = empty[A] }
+ override def addOne(elem: A): this.type = { res = res.incl(elem); this }
+ override def result(): Linear_Set[A] = res
+ }
class Duplicate[A](x: A) extends Exception
class Undefined[A](x: A) extends Exception
@@ -30,13 +37,10 @@
final class Linear_Set[A] private(
start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
- extends scala.collection.immutable.Set[A]
- with GenericSetTemplate[A, Linear_Set]
- with SetLike[A, Linear_Set[A]]
+ extends Iterable[A]
+ with SetOps[A, Linear_Set, Linear_Set[A]]
+ with IterableFactoryDefaults[A, Linear_Set]
{
- override def companion: GenericCompanion[Linear_Set] = Linear_Set
-
-
/* relative addressing */
def next(elem: A): Option[A] =
@@ -78,7 +82,7 @@
}
}
- def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] = // FIXME reverse fold
+ def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold
((hook, this) /: elems) {
case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
}._2
@@ -115,8 +119,6 @@
/* Set methods */
- override def stringPrefix = "Linear_Set"
-
override def isEmpty: Boolean = start.isEmpty
override def size: Int = if (isEmpty) 0 else nexts.size + 1
@@ -153,7 +155,10 @@
override def last: A = reverse.head
- def + (elem: A): Linear_Set[A] = insert_after(end, elem)
+ def incl(elem: A): Linear_Set[A] = insert_after(end, elem)
+ def excl(elem: A): Linear_Set[A] = delete_after(prev(elem))
- def - (elem: A): Linear_Set[A] = delete_after(prev(elem))
+ override def iterableFactory: IterableFactory[Linear_Set] = Linear_Set
+
+ override def toString: String = mkString("Linear_Set(", ", ", ")")
}
--- a/src/Pure/General/multi_map.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/General/multi_map.scala Sat Jan 16 22:52:43 2021 +0100
@@ -6,24 +6,33 @@
package isabelle
-
-import scala.collection.GenTraversableOnce
-import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
+import scala.collection.mutable
+import scala.collection.{IterableFactory, MapFactory, MapFactoryDefaults}
+import scala.collection.immutable.{Iterable, MapOps}
-object Multi_Map extends ImmutableMapFactory[Multi_Map]
+object Multi_Map extends MapFactory[Multi_Map]
{
private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
- override def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+ def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+
+ def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] =
+ (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) })
- implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
- new MapCanBuildFrom[A, B]
+ override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B]
+ private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]
+ {
+ private var res = empty[A, B]
+ override def clear() { res = empty[A, B] }
+ override def addOne(p: (A, B)): this.type = { res = res.insert(p._1, p._2); this }
+ override def result(): Multi_Map[A, B] = res
+ }
}
-
final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]])
- extends scala.collection.immutable.Map[A, B]
- with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
+ extends Iterable[(A, B)]
+ with MapOps[A, B, Multi_Map, Multi_Map[A, B]]
+ with MapFactoryDefaults[A, B, Multi_Map, Iterable]
{
/* Multi_Map operations */
@@ -61,8 +70,6 @@
/* Map operations */
- override def stringPrefix = "Multi_Map"
-
override def empty: Multi_Map[A, Nothing] = Multi_Map.empty
override def isEmpty: Boolean = rep.isEmpty
@@ -73,11 +80,12 @@
def get(a: A): Option[B] = get_list(a).headOption
- def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
+ override def updated[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = insert(a, b)
+
+ override def removed(a: A): Multi_Map[A, B] =
+ if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
- override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
- (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
+ override def mapFactory: MapFactory[Multi_Map] = Multi_Map
- def - (a: A): Multi_Map[A, B] =
- if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
+ override def toString: String = mkString("Multi_Map(", ", ", ")")
}
--- a/src/Pure/General/scan.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/General/scan.scala Sat Jan 16 22:52:43 2021 +0100
@@ -9,10 +9,9 @@
import scala.annotation.tailrec
import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
-import scala.collection.immutable.PagedSeq
import scala.util.matching.Regex
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
- Reader, CharSequenceReader}
+ Reader, CharSequenceReader, PagedSeq}
import scala.util.parsing.combinator.RegexParsers
import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
import java.net.URL
--- a/src/Pure/ROOT.ML Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/ROOT.ML Sat Jan 16 22:52:43 2021 +0100
@@ -354,3 +354,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
+
--- a/src/Pure/ROOT.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/ROOT.scala Sat Jan 16 22:52:43 2021 +0100
@@ -21,3 +21,4 @@
val proper_string = Library.proper_string _
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
}
+
--- a/src/Pure/System/scala.scala Sat Jan 16 19:25:20 2021 +0100
+++ b/src/Pure/System/scala.scala Sat Jan 16 22:52:43 2021 +0100
@@ -11,7 +11,7 @@
import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
import scala.tools.nsc.interpreter.{IMain, Results}
-
+import scala.tools.nsc.interpreter.shell.ReplReporterImpl
object Scala
{
@@ -96,7 +96,7 @@
print_writer: PrintWriter = default_print_writer,
class_loader: ClassLoader = null): IMain =
{
- new IMain(settings, print_writer)
+ new IMain(settings, new ReplReporterImpl(settings, print_writer))
{
override def parentClassLoader: ClassLoader =
if (class_loader == null) super.parentClassLoader