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 _ => ??? }
   }