src/Pure/Thy/thy_header.scala
changeset 43697 77ce24aa1770
parent 43695 5130dfe1b7be
child 43699 fb3d99df4b1e
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jul 07 14:10:50 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jul 07 22:04:30 2011 +0200
     1.3 @@ -38,14 +38,10 @@
     1.4  
     1.5    def thy_path(name: String): Path = Path.basic(name).ext("thy")
     1.6  
     1.7 -  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
     1.8 -  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
     1.9 -
    1.10 -  def split_thy_path(path: String): Option[(String, String)] =
    1.11 -    path match {
    1.12 -      case Thy_Path1(name) => Some(("", name))
    1.13 -      case Thy_Path2(dir, name) => Some((dir, name))
    1.14 -      case _ => None
    1.15 +  def split_thy_path(path: Path): (Path, String) =
    1.16 +    path.split_ext match {
    1.17 +      case (path1, "thy") => (path1.dir, path1.base.implode)
    1.18 +      case _ => error("Bad theory file specification: " + path)
    1.19      }
    1.20  
    1.21