src/Pure/Thy/thy_header.scala
changeset 44225 a8f921e6484f
parent 44222 9d5ef6cd4ee1
child 44578 ca3844a3dcf7
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 21:54:06 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 22:48:31 2011 +0200
     1.3 @@ -28,8 +28,12 @@
     1.4  
     1.5    /* theory file name */
     1.6  
     1.7 +  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
     1.8    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     1.9  
    1.10 +  def base_name(s: String): String =
    1.11 +    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    1.12 +
    1.13    def thy_name(s: String): Option[String] =
    1.14      s match { case Thy_Name(name) => Some(name) case _ => None }
    1.15