src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Mon Dec 07 22:28:41 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Dec 08 16:30:17 2020 +0100
@@ -90,6 +90,12 @@
       case _ => None
     }
 
+  def dir_name(s: String): String =
+    split_file_name(s) match {
+      case Some((dir, _)) => dir
+      case None => ""
+    }
+
   def import_name(s: String): String =
     s match {
       case File_Name(name) if !name.endsWith(".thy") => name