# HG changeset patch
# User wenzelm
# Date 1635864002 -3600
# Node ID 9fcf80ceb863cbe84576ee319b4d38213d8f505c
# Parent  0659536b150be16fc74ebb0c925e452ec0e3ee76
updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;

diff -r 0659536b150b -r 9fcf80ceb863 Admin/components/components.sha1
--- 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
diff -r 0659536b150b -r 9fcf80ceb863 Admin/components/main
--- 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
diff -r 0659536b150b -r 9fcf80ceb863 src/HOL/Tools/Mirabelle/mirabelle.scala
--- 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  "
diff -r 0659536b150b -r 9fcf80ceb863 src/Pure/PIDE/session.scala
--- 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) =>
diff -r 0659536b150b -r 9fcf80ceb863 src/Pure/Thy/export_theory.scala
--- 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
diff -r 0659536b150b -r 9fcf80ceb863 src/Pure/Thy/html.scala
--- 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)) }))
 
diff -r 0659536b150b -r 9fcf80ceb863 src/Pure/Tools/build_job.scala
--- 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