# HG changeset patch
# User wenzelm
# Date 1610833963 -3600
# Node ID ca17e9ebfdf17a7294f05d14134bff52b5a672cb
# Parent  76bdfde8a579a8512e03b5cf4631c5550d6a3054
updated to scala-2.13.4;

diff -r 76bdfde8a579 -r ca17e9ebfdf1 Admin/components/components.sha1
--- 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
diff -r 76bdfde8a579 -r ca17e9ebfdf1 Admin/components/main
--- 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
diff -r 76bdfde8a579 -r ca17e9ebfdf1 etc/settings
--- 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"
 
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/General/linear_set.scala
--- 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(", ", ", ")")
 }
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/General/multi_map.scala
--- 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(", ", ", ")")
 }
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/General/scan.scala
--- 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
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/ROOT.ML
--- 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"
+
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/ROOT.scala
--- 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)
 }
+
diff -r 76bdfde8a579 -r ca17e9ebfdf1 src/Pure/System/scala.scala
--- 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