src/Pure/Thy/thy_header.scala
changeset 43648 e32de528b5ef
parent 43646 598b2c6ce13f
child 43652 dcd0b667f73d
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 03 15:10:17 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 03 19:42:32 2011 +0200
     1.3 @@ -36,8 +36,10 @@
     1.4  
     1.5    /* file name */
     1.6  
     1.7 -  val Thy_Path1 = new Regex("([^/]*)\\.thy")
     1.8 -  val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
     1.9 +  def thy_path(name: String): Path = Path.basic(name).ext("thy")
    1.10 +
    1.11 +  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
    1.12 +  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
    1.13  
    1.14    def split_thy_path(path: String): Option[(String, String)] =
    1.15      path match {
    1.16 @@ -108,4 +110,15 @@
    1.17      try { read(reader).decode_permissive_utf8 }
    1.18      finally { reader.close }
    1.19    }
    1.20 +
    1.21 +
    1.22 +  /* check */
    1.23 +
    1.24 +  def check(name: String, source: CharSequence): Header =
    1.25 +  {
    1.26 +    val header = read(source)
    1.27 +    val name1 = header.name
    1.28 +    if (name == name1) header
    1.29 +    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
    1.30 +  }
    1.31  }