# 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