diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/General/file.scala
--- 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] = {