diff -r 6fd8e482c9ce -r 7bf685cbc789 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Feb 21 20:31:30 2022 +0100
+++ b/src/Pure/General/path.scala	Mon Feb 21 20:50:01 2022 +0100
@@ -215,6 +215,7 @@
     }
   def is_java: Boolean = ends_with(".java")
   def is_scala: Boolean = ends_with(".scala")
+  def is_pdf: Boolean = ends_with(".pdf")
 
   def ext(e: String): Path =
     if (e == "") this