# HG changeset patch
# User wenzelm
# Date 1649498558 -7200
# Node ID b958e053d9939e3dfb50b34fbf4610e8e495126d
# Parent  5f8f0bf8c72c2b366a360ef8192912180f26dcf2
avoid pattern-match warnings, notably in scala3;

diff -r 5f8f0bf8c72c -r b958e053d993 etc/settings
--- a/etc/settings	Sat Apr 09 11:56:48 2022 +0200
+++ b/etc/settings	Sat Apr 09 12:02:38 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 5f8f0bf8c72c -r b958e053d993 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Apr 09 12:02:38 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 5f8f0bf8c72c -r b958e053d993 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat Apr 09 12:02:38 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 5f8f0bf8c72c -r b958e053d993 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Sat Apr 09 12:02:38 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 5f8f0bf8c72c -r b958e053d993 src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Pure/term_xml.scala	Sat Apr 09 12:02:38 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 (a, b) => TVar(indexname(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)) case _ => ??? }))
 
     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 (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 (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 _ => ??? },
+        { 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 (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 (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 _ => ??? },
+          { 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 5f8f0bf8c72c -r b958e053d993 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 12:02:38 2022 +0200
@@ -140,6 +140,7 @@
                 (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)
             }
diff -r 5f8f0bf8c72c -r b958e053d993 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 09 12:02:38 2022 +0200
@@ -125,6 +125,7 @@
                 m.x - slack * dx2, m.y - slack * dy2,
                 m.x, m.y)
               (dx2, dy2)
+            case _ => ???
           }
 
         val l = ds.last