--- a/src/Pure/General/file.scala Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/General/file.scala Fri Aug 19 16:46:00 2022 +0200
@@ -69,6 +69,26 @@
def url(path: Path): URL = url(path.file)
+ /* adhoc file types */
+
+ def is_ML(s: String): Boolean = s.endsWith(".ML")
+ def is_bib(s: String): Boolean = s.endsWith(".bib")
+ def is_dll(s: String): Boolean = s.endsWith(".dll")
+ def is_exe(s: String): Boolean = s.endsWith(".exe")
+ def is_gz(s: String): Boolean = s.endsWith(".gz")
+ def is_html(s: String): Boolean = s.endsWith(".html")
+ def is_jar(s: String): Boolean = s.endsWith(".jar")
+ def is_java(s: String): Boolean = s.endsWith(".java")
+ def is_node(s: String): Boolean = s.endsWith(".node")
+ def is_pdf(s: String): Boolean = s.endsWith(".pdf")
+ def is_png(s: String): Boolean = s.endsWith(".png")
+ def is_thy(s: String): Boolean = s.endsWith(".thy")
+ def is_xz(s: String): Boolean = s.endsWith(".xz")
+ def is_zip(s: String): Boolean = s.endsWith(".zip")
+
+ def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig")
+
+
/* relative paths */
def relative_path(base: Path, other: Path): Option[Path] = {