more robust: avoid partiality;

--- a/src/Pure/System/isabelle_system.scala	Sat Apr 09 15:35:27 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Apr 09 15:40:29 2022 +0200
@@ -484,7 +484,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) case _ => ??? }
+      args.map(url => download(url.text).bytes)
   }
 
 

--- a/src/Tools/Graphview/layout.scala	Sat Apr 09 15:35:27 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Sat Apr 09 15:40:29 2022 +0200
@@ -140,7 +140,7 @@
                 (v1 :: dummies ::: List(v2)).sliding(2)
                   .foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
                     case (g, Seq(a, b)) => g.add_edge(a, b)
-                    case _ => ???
+                    case (g, _) => g
                   }
               (graph1, levels1)
             }

--- a/src/Tools/Graphview/shapes.scala	Sat Apr 09 15:35:27 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Sat Apr 09 15:40:29 2022 +0200
@@ -125,7 +125,7 @@
                 m.x - slack * dx2, m.y - slack * dy2,
                 m.x, m.y)
               (dx2, dy2)
-            case _ => ???
+            case (p, _) => p
           }
 
         val l = ds.last