src/Pure/Thy/thy_header.scala
changeset 39630 44181423183a
parent 38149 3c380380beac
child 41535 0112f14d75ec
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Sep 23 16:48:48 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Sep 23 18:44:26 2010 +0200
     1.3 @@ -32,11 +32,11 @@
     1.4    val Thy_Path1 = new Regex("([^/]*)\\.thy")
     1.5    val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
     1.6  
     1.7 -  def split_thy_path(path: String): (String, String) =
     1.8 +  def split_thy_path(path: String): Option[(String, String)] =
     1.9      path match {
    1.10 -      case Thy_Path1(name) => ("", name)
    1.11 -      case Thy_Path2(dir, name) => (dir, name)
    1.12 -      case _ => error("Bad theory file specification: " + path)
    1.13 +      case Thy_Path1(name) => Some(("", name))
    1.14 +      case Thy_Path2(dir, name) => Some((dir, name))
    1.15 +      case _ => None
    1.16      }
    1.17  }
    1.18