src/Pure/General/path.scala

 Algebra of file-system paths: basic POSIX notation, extended by named
 roots (e.g. //foo) and variables (e.g. $BAR).
 */
 
 package isabelle
+
+
+import scala.util.matching.Regex
 
 
 object Path
 {
   /* path elements */

     else {
       val (prfx, s) = split_path
       prfx + Path.basic(s + "." + e)
     }
 
+  private val Ext = new Regex("(.*)\\.([^.]*)")
+
+  def split_ext: (Path, String) =
+  {
+    val (prefix, base) = split_path
+    base match {
+      case Ext(b, e) => (prefix + Path.basic(b), e)
+      case _ => (Path.basic(base), "")
+    }
+  }
+
 
   /* expand */
 
   def expand: Path =
   {