# HG changeset patch # User wenzelm # Date 1649511218 -7200 # Node ID 7b417c578b19dd338565d539bc1a9179be7dbb58 # Parent 40630fec3b5dda13bee3da7f930c31bbedd577df clarified signature; diff -r 40630fec3b5d -r 7b417c578b19 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Apr 09 15:28:55 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Apr 09 15:33:38 2022 +0200 @@ -143,19 +143,22 @@ /* scala functions */ - private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] = { + private def apply_paths( + args: List[String], + fun: PartialFunction[List[Path], Unit] + ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = - apply_paths(args, { case List(path) => fun(path) case _ => ??? }) + apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = - apply_paths(args, { case List(path1, path2) => fun(path1, path2) case _ => ??? }) + apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) 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) case _ => ??? }) + apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */