src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Wed Aug 04 16:28:45 2010 +0200
+++ b/src/Pure/Thy/thy_header.scala	Thu Aug 05 13:41:00 2010 +0200
@@ -9,6 +9,7 @@
 
 import scala.collection.mutable
 import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.matching.Regex
 
 import java.io.File
 
@@ -24,6 +25,19 @@
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
   final case class Header(val name: String, val imports: List[String], val uses: List[String])
+
+
+  /* file name */
+
+  val Thy_Path1 = new Regex("([^/]*)\\.thy")
+  val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
+
+  def split_thy_path(path: String): (String, String) =
+    path match {
+      case Thy_Path1(name) => ("", name)
+      case Thy_Path2(dir, name) => (dir, name)
+      case _ => error("Bad theory file specification: " + path)
+    }
 }