src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -26,16 +26,15 @@
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
 
-  /* file name */
+  /* theory file name */
+
+  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+
+  def thy_name(s: String): Option[String] =
+    s match { case Thy_Name(name) => Some(name) case _ => None }
 
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
-  def split_thy_path(path: Path): (Path, String) =
-    path.split_ext match {
-      case (path1, "thy") => (path1.dir, path1.base.implode)
-      case _ => error("Bad theory file specification: " + path)
-    }
-
 
   /* header */