# HG changeset patch
# User wenzelm
# Date 1649511629 -7200
# Node ID e1c9e4d599210ceb1ebfad3065df43f4533c0fe4
# Parent  96293bd077bb6570832993e60980cddb8287e702
more robust: avoid partiality;

diff -r 96293bd077bb -r e1c9e4d59921 src/Pure/System/isabelle_system.scala
--- 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)
   }
 
 
diff -r 96293bd077bb -r e1c9e4d59921 src/Tools/Graphview/layout.scala
--- 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)
             }
diff -r 96293bd077bb -r e1c9e4d59921 src/Tools/Graphview/shapes.scala
--- 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