src/Pure/Thy/thy_header.scala
changeset 44222 9d5ef6cd4ee1
parent 44185 05641edb5d30
child 44225 a8f921e6484f
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 16 12:06:49 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 16 21:13:52 2011 +0200
     1.3 @@ -28,11 +28,12 @@
     1.4  
     1.5    /* theory file name */
     1.6  
     1.7 -  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
     1.8 +  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     1.9  
    1.10 -  def thy_name(s: String): Option[(String, String)] =
    1.11 -    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
    1.12 +  def thy_name(s: String): Option[String] =
    1.13 +    s match { case Thy_Name(name) => Some(name) case _ => None }
    1.14  
    1.15 +  def thy_path(path: Path): Path = path.ext("thy")
    1.16    def thy_path(name: String): Path = Path.basic(name).ext("thy")
    1.17  
    1.18  
    1.19 @@ -113,7 +114,7 @@
    1.20    def map(f: String => String): Thy_Header =
    1.21      Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
    1.22  
    1.23 -  def norm_deps(f: String => String): Thy_Header =
    1.24 -    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
    1.25 +  def norm_deps(f: String => String, g: String => String): Thy_Header =
    1.26 +    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
    1.27  }
    1.28