updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;
--- a/Admin/components/components.sha1 Tue Nov 02 14:05:02 2021 +0100
+++ b/Admin/components/components.sha1 Tue Nov 02 15:40:02 2021 +0100
@@ -385,6 +385,7 @@
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
+1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.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 Tue Nov 02 14:05:02 2021 +0100
+++ b/Admin/components/main Tue Nov 02 15:40:02 2021 +0100
@@ -19,7 +19,7 @@
opam-2.0.7
polyml-5.9-960de0cd0795
postgresql-42.2.24
-scala-2.13.5
+scala-2.13.7
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Nov 02 14:05:02 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Nov 02 15:40:02 2021 +0100
@@ -85,7 +85,7 @@
}
using(store.open_database_context())(db_context =>
{
- for (export <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
+ for (`export` <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
val prefix = args.name.split('/') match {
case Array("mirabelle", action, "finalize") =>
s"${action} finalize "
--- a/src/Pure/PIDE/session.scala Tue Nov 02 14:05:02 2021 +0100
+++ b/src/Pure/PIDE/session.scala Tue Nov 02 15:40:02 2021 +0100
@@ -507,7 +507,7 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
- val export = Export.make_entry("", args, msg.chunk, cache)
+ val `export` = Export.make_entry("", args, msg.chunk, cache)
change_command(_.add_export(id, (args.serial, export)))
case Protocol.Loading_Theory(node_name, id) =>
--- a/src/Pure/Thy/export_theory.scala Tue Nov 02 14:05:02 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Tue Nov 02 15:40:02 2021 +0100
@@ -183,7 +183,7 @@
val DOCUMENT_TEXT = "document_text"
val PROOF_TEXT = "proof_text"
- def export(kind: String): String =
+ def `export`(kind: String): String =
kind match {
case Markup.TYPE_NAME => TYPE
case Markup.CONSTANT => CONST
--- a/src/Pure/Thy/html.scala Tue Nov 02 14:05:02 2021 +0100
+++ b/src/Pure/Thy/html.scala Tue Nov 02 15:40:02 2021 +0100
@@ -56,7 +56,7 @@
val code = new Operator("code")
val item = new Operator("li")
val list = new Operator("ul")
- val enum = new Operator("ol")
+ val `enum` = new Operator("ol")
val descr = new Operator("dl")
val dt = new Operator("dt")
val dd = new Operator("dd")
@@ -70,7 +70,7 @@
val subparagraph = new Heading("h6")
def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
- def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
+ def enumerate(items: List[XML.Body]): XML.Elem = `enum`(items.map(item(_)))
def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
--- a/src/Pure/Tools/build_job.scala Tue Nov 02 14:05:02 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Nov 02 15:40:02 2021 +0100
@@ -325,7 +325,7 @@
case _ => false
}
- private def export(msg: Prover.Protocol_Output): Boolean =
+ private def `export`(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Protocol.Export(args) =>
export_consumer(session_name, args, msg.chunk)
@@ -364,7 +364,7 @@
if (!progress.stopped) {
val rendering = new Rendering(snapshot, options, session)
- def export(name: String, xml: XML.Body, compress: Boolean = true): Unit =
+ def `export`(name: String, xml: XML.Body, compress: Boolean = true): Unit =
{
if (!progress.stopped) {
val theory_name = snapshot.node_name.theory