# HG changeset patch
# User wenzelm
# Date 1281008460 -7200
# Node ID 3c380380beac22413691e0498b78ba8dcdeb763b
# Parent  d2f3c8d4a89f82630582412eb12b68ef95f8f473
somewhat uniform Thy_Header.split_thy_path in ML and Scala;

diff -r d2f3c8d4a89f -r 3c380380beac src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Aug 04 16:28:45 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Thu Aug 05 13:41:00 2010 +0200
@@ -68,14 +68,14 @@
   end;
 
 
-(* file formats *)
+(* file name *)
 
 val thy_path = Path.ext "thy" o Path.basic;
 
 fun split_thy_path path =
   (case Path.split_ext path of
     (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
-  | _ => error ("Bad theory file specification " ^ Path.implode path));
+  | _ => error ("Bad theory file specification: " ^ Path.implode path));
 
 fun consistent_name name name' =
   if name = name' then ()
diff -r d2f3c8d4a89f -r 3c380380beac 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)
+    }
 }