diff -r 0ee44ed80290 -r fb8d5c0133c9 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Jul 24 13:09:48 2021 +0200
+++ b/src/Pure/General/path.scala	Sat Jul 24 15:38:41 2021 +0200
@@ -207,6 +207,14 @@
   def dir: Path = split_path._1
   def base: Path = new Path(List(Path.Basic(split_path._2)))
 
+  def ends_with(a: String): Boolean =
+    elems match {
+      case Path.Basic(b) :: _ => b.endsWith(a)
+      case _ => false
+    }
+  def is_java: Boolean = ends_with(".java")
+  def is_scala: Boolean = ends_with(".scala")
+
   def ext(e: String): Path =
     if (e == "") this
     else {