# HG changeset patch
# User wenzelm
# Date 1649499017 -7200
# Node ID d5dd932552c0ad888447c7eb15a97ce5d3dd1d41
# Parent  e0fa345f1aab0b34c625a0a713deedded5a1d2a3# Parent  323481d143c6ec49a153646133ffb73136f00965
merged

diff -r e0fa345f1aab -r d5dd932552c0 etc/settings
--- a/etc/settings	Sat Apr 09 11:40:42 2022 +0200
+++ b/etc/settings	Sat Apr 09 12:10:17 2022 +0200
@@ -17,7 +17,7 @@
 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
 
 ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11"
-ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m"
+ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m"
 
 ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar"
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Admin/build_scala.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -43,22 +43,22 @@
   }
 
   val main_download: Download =
-    Download("scala", "3.0.2", base_version = "",
+    Download("scala", "3.1.1", base_version = "",
       url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
 
   val lib_downloads: List[Download] = List(
     Download("scala-parallel-collections", "1.0.4",
       "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
       physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
-    Download("scala-parser-combinators", "2.1.0",
+    Download("scala-parser-combinators", "2.1.1",
       "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
       physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
     Download("scala-swing", "3.0.0",
       "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-swing_{B}/{V}",
       physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-swing_{B}/{V}/scala-swing_{B}-{V}.jar"),
-    Download("scala-xml", "2.0.1",
+    Download("scala-xml", "2.1.0",
       "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-xml_{B}/{V}",
-      physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_3/2.0.1/scala-xml_{B}-{V}.jar")
+      physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_{B}/{V}/scala-xml_{B}-{V}.jar")
   )
 
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/General/antiquote.scala
--- a/src/Pure/General/antiquote.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/General/antiquote.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -44,7 +44,8 @@
   /* read */
 
   def read(input: CharSequence): List[Antiquote] = {
-    Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match {
+    val result = Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input))
+    (result : @unchecked) match {
       case Parsers.Success(xs, _) => xs
       case Parsers.NoSuccess(_, next) =>
         error("Malformed quotation/antiquotation source" +
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/General/json.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -145,7 +145,8 @@
 
     def parse(input: CharSequence, strict: Boolean): T = {
       val scanner = new Lexer.Scanner(Scan.char_reader(input))
-      phrase(if (strict) json_object | json_array else json_value)(scanner) match {
+      val result = phrase(if (strict) json_object | json_array else json_value)(scanner)
+      (result : @unchecked) match {
         case Success(json, _) => json
         case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos)
       }
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Isar/token.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -140,7 +140,8 @@
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
-      Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {
+      val result = Parsers.parse(Parsers.token_line(keywords, ctxt), in)
+      (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -281,7 +281,8 @@
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
-      Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
+      val result = Parsers.parse(Parsers.token_line(SML, ctxt), in)
+      (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -563,7 +563,6 @@
             case (res, Text.Info(_, elem)) =>
               Command.State.get_result_proper(command_states, elem.markup.properties)
                 .map(res :+ _)
-            case _ => None
           })
 
     var seen_serials = Set.empty[Long]
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -149,13 +149,13 @@
   }
 
   private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
-    apply_paths(args, { case List(path) => fun(path) })
+    apply_paths(args, { case List(path) => fun(path) case _ => ??? })
 
   private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
-    apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
+    apply_paths(args, { case List(path1, path2) => fun(path1, path2) case _ => ??? })
 
   private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
-    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
+    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) case _ => ??? })
 
 
   /* permissions */
@@ -481,7 +481,7 @@
   object Download extends Scala.Fun("download", thread = true) {
     val here = Scala_Project.here
     override def invoke(args: List[Bytes]): List[Bytes] =
-      args match { case List(url) => List(download(url.text).bytes) }
+      args match { case List(url) => List(download(url.text).bytes) case _ => ??? }
   }
 
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/System/scala.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -112,15 +112,11 @@
         }
       }
 
-      def toplevel(interpret: Boolean, source: String): List[String] = {
+      def toplevel(source: String): List[String] = {
         val out = new StringWriter
         val interp = interpreter(new PrintWriter(out))
         val marker = '\u000b'
-        val ok =
-          interp.withLabel(marker.toString) {
-            if (interpret) interp.interpret(source) == Results.Success
-            else (new interp.ReadEvalPrint).compile(source)
-          }
+        val ok = interp.withLabel(marker.toString) { (new interp.ReadEvalPrint).compile(source) }
         out.close()
 
         val Error = """(?s)^\S* error: (.*)$""".r
@@ -135,15 +131,9 @@
 
   object Toplevel extends Fun_String("scala_toplevel") {
     val here = Scala_Project.here
-    def apply(arg: String): String = {
-      val (interpret, source) =
-        YXML.parse_body(arg) match {
-          case Nil => (false, "")
-          case List(XML.Text(source)) => (false, source)
-          case body => import XML.Decode._; pair(bool, string)(body)
-        }
+    def apply(source: String): String = {
       val errors =
-        try { Compiler.context().toplevel(interpret, source) }
+        try { Compiler.context().toplevel(source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/System/scala_compiler.ML	Sat Apr 09 12:10:17 2022 +0200
@@ -6,7 +6,7 @@
 
 signature SCALA_COMPILER =
 sig
-  val toplevel: bool -> string -> unit
+  val toplevel: string -> unit
   val static_check: string * Position.T -> unit
 end;
 
@@ -15,18 +15,15 @@
 
 (* check declaration *)
 
-fun toplevel interpret source =
+fun toplevel source =
   let val errors =
-    (interpret, source)
-    |> let open XML.Encode in pair bool string end
-    |> YXML.string_of_body
-    |> \<^scala>\<open>scala_toplevel\<close>
+    \<^scala>\<open>scala_toplevel\<close> source
     |> YXML.parse_body
     |> let open XML.Decode in list string end
   in if null errors then () else error (cat_lines errors) end;
 
 fun static_check (source, pos) =
-  toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
+  toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
     handle ERROR msg => error (msg ^ Position.here pos);
 
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -599,7 +599,8 @@
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
-      Parsers.parse(Parsers.chunk_line(ctxt), in) match {
+      val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
+      (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unepected failure to parse input:\n" + rest.source.toString)
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -264,12 +264,13 @@
 
   def decode_syntax: XML.Decode.T[Syntax] =
     XML.Decode.variant(List(
-      { case (Nil, Nil) => No_Syntax },
-      { case (List(delim), Nil) => Prefix(delim) },
+      { case (Nil, Nil) => No_Syntax case _ => ??? },
+      { case (List(delim), Nil) => Prefix(delim) case _ => ??? },
       { case (Nil, body) =>
           import XML.Decode._
           val (ass, delim, pri) = triple(int, string, int)(body)
-          Infix(Assoc(ass), delim, pri) }))
+          Infix(Assoc(ass), delim, pri)
+        case _ => ??? }))
 
 
   /* types */
@@ -684,11 +685,11 @@
   val decode_recursion: XML.Decode.T[Recursion] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Primrec(list(string)(a)) },
-      { case (Nil, Nil) => Recdef },
-      { case (Nil, a) => Primcorec(list(string)(a)) },
-      { case (Nil, Nil) => Corec },
-      { case (Nil, Nil) => Unknown_Recursion }))
+      { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? },
+      { case (Nil, Nil) => Recdef case _ => ??? },
+      { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? },
+      { case (Nil, Nil) => Corec case _ => ??? },
+      { case (Nil, Nil) => Unknown_Recursion case _ => ??? }))
   }
 
 
@@ -713,10 +714,10 @@
   val decode_rough_classification: XML.Decode.T[Rough_Classification] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Equational(decode_recursion(a)) },
-      { case (Nil, Nil) => Inductive },
-      { case (Nil, Nil) => Co_Inductive },
-      { case (Nil, Nil) => Unknown }))
+      { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? },
+      { case (Nil, Nil) => Inductive case _ => ??? },
+      { case (Nil, Nil) => Co_Inductive case _ => ??? },
+      { case (Nil, Nil) => Unknown case _ => ??? }))
   }
 
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -463,7 +463,11 @@
 
       val result = {
         val theory_timing =
-          theory_timings.iterator.map({ case props @ Markup.Name(name) => name -> props }).toMap
+          theory_timings.iterator.map(
+            {
+              case props @ Markup.Name(name) => name -> props
+              case _ => ???
+            }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }
             yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Tools/scala_project.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -11,8 +11,8 @@
 object Scala_Project {
   /** build tools **/
 
-  def java_version: String = "15"
-  def scala_version: String = scala.util.Properties.versionNumberString
+  val java_version: String = "17"
+  val scala_version: String = "2.13.5"
 
   abstract class Build_Tool {
     def project_root: Path
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Tools/server.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -348,11 +348,7 @@
           }
         }
       }
-      catch {
-        case _: IOException => false
-        case _: SocketException => false
-        case _: SocketTimeoutException => false
-      }
+      catch { case _: IOException => false }
   }
 
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/term_xml.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -48,20 +48,20 @@
 
     def typ: T[Typ] =
       variant[Typ](List(
-        { case (List(a), b) => Type(a, list(typ)(b)) },
-        { case (List(a), b) => TFree(a, sort(b)) },
+        { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? },
+        { case (List(a), b) => TFree(a, sort(b)) case _ => ??? },
         { case (a, b) => TVar(indexname(a), sort(b)) }))
 
     val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
     def term: T[Term] =
       variant[Term](List(
-        { case (List(a), b) => Const(a, list(typ)(b)) },
-        { case (List(a), b) => Free(a, typ_body(b)) },
+        { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
+        { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? },
         { case (a, b) => Var(indexname(a), typ_body(b)) },
-        { case (Nil, a) => Bound(int(a)) },
-        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
-        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+        { case (Nil, a) => Bound(int(a)) case _ => ??? },
+        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
+        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))
 
     def term_env(env: Map[String, Typ]): T[Term] = {
       def env_type(x: String, t: Typ): Typ =
@@ -69,12 +69,12 @@
 
       def term: T[Term] =
         variant[Term](List(
-          { case (List(a), b) => Const(a, list(typ)(b)) },
-          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
+          { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
+          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? },
           { case (a, b) => Var(indexname(a), typ_body(b)) },
-          { case (Nil, a) => Bound(int(a)) },
-          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
-          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+          { case (Nil, a) => Bound(int(a)) case _ => ??? },
+          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
+          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))
       term
     }
 
@@ -82,17 +82,17 @@
       val term = term_env(env)
       def proof: T[Proof] =
         variant[Proof](List(
-          { case (Nil, Nil) => MinProof },
-          { case (Nil, a) => PBound(int(a)) },
-          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
-          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
-          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
-          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
-          { case (Nil, a) => Hyp(term(a)) },
-          { case (List(a), b) => PAxm(a, list(typ)(b)) },
-          { case (List(a), b) => PClass(typ(b), a) },
-          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
-          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+          { case (Nil, Nil) => MinProof case _ => ??? },
+          { case (Nil, a) => PBound(int(a)) case _ => ??? },
+          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? },
+          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? },
+          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? },
+          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? },
+          { case (Nil, a) => Hyp(term(a)) case _ => ??? },
+          { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? },
+          { case (List(a), b) => PClass(typ(b), a) case _ => ??? },
+          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? },
+          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? }))
       proof
     }
 
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -137,9 +137,10 @@
 
               val levels1 = dummies_levels.foldLeft(levels)(_ + _)
               val graph1 =
-                (v1 :: dummies ::: List(v2)).sliding(2).
+                (v1 :: dummies ::: List(v2)).sliding(2).map(_.toList).
                   foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
                     case (g, List(a, b)) => g.add_edge(a, b)
+                    case _ => ???
                   }
               (graph1, levels1)
             }
@@ -235,7 +236,7 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-    levels.iterator.sliding(2).map {
+    levels.iterator.sliding(2).map(_.toList).map {
       case List(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/popups.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -30,25 +30,25 @@
       new Menu(caption) {
         contents +=
           new MenuItem(new Action("This") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false)))
           })
 
         contents +=
           new MenuItem(new Action("Family") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true)))
           })
 
         contents +=
           new MenuItem(new Action("Parents") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true)))
           })
 
         contents +=
           new MenuItem(new Action("Children") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false)))
           })
 
@@ -77,7 +77,7 @@
                           contents +=
                             new MenuItem(
                               new Action(quote(to.toString)) {
-                                def apply =
+                                def apply(): Unit =
                                   add_mutator(
                                     Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                               })
@@ -96,7 +96,7 @@
                           contents +=
                             new MenuItem(
                               new Action(quote(from.toString)) {
-                                def apply =
+                                def apply(): Unit =
                                   add_mutator(
                                     Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                               })
@@ -113,7 +113,7 @@
 
     popup.add(
       new MenuItem(
-        new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer)
+        new Action("Remove all filters") { def apply(): Unit = graphview.model.Mutators(Nil) }).peer)
     popup.add(new JPopupMenu.Separator)
 
     if (mouse_node.isDefined) {
@@ -138,7 +138,7 @@
     }
 
     popup.add(new MenuItem(new Action("Fit to window") {
-      def apply = graph_panel.fit_to_window() }).peer
+      def apply(): Unit = graph_panel.fit_to_window() }).peer
     )
 
     popup
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -116,7 +116,7 @@
         val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          coords.sliding(3).foldLeft((dx, dy)) {
+          coords.sliding(3).map(_.toList).foldLeft((dx, dy)) {
             case ((dx, dy), List(l, m, r)) =>
               val dx2 = r.x - l.x
               val dy2 = r.y - l.y
@@ -125,6 +125,7 @@
                 m.x - slack * dx2, m.y - slack * dy2,
                 m.x, m.y)
               (dx2, dy2)
+            case _ => ???
           }
 
         val l = ds.last
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -143,8 +143,6 @@
 
             case (res, Text.Info(_, msg)) =>
               Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
-
-            case _ => None
           }).filterNot(info => info.info.is_empty)
 
   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = {
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -353,7 +353,6 @@
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
-          case _ => None
         }).map(_.info)
 
     gutter_message_content.get(pris.foldLeft(0)(_ max _))
diff -r e0fa345f1aab -r d5dd932552c0 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Sat Apr 09 12:10:17 2022 +0200
@@ -107,7 +107,7 @@
 
           def indent_indent(tok: Token): Int =
             if (keywords.is_command(tok, keyword_open)) indent_size
-            else if (keywords.is_command(tok, keyword_close)) - indent_size
+            else if (keywords.is_command(tok, keyword_close)) { - indent_size }
             else 0
 
           def indent_offset(tok: Token): Int =