src/Pure/Thy/thy_header.scala
changeset 46737 09ab89658a5d
parent 46676 b4bc54d4624b
child 46938 cda018294515
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Feb 29 17:43:41 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Feb 29 23:09:06 2012 +0100
     1.3 @@ -37,8 +37,6 @@
     1.4    def thy_name(s: String): Option[String] =
     1.5      s match { case Thy_Name(name) => Some(name) case _ => None }
     1.6  
     1.7 -  def thy_path(path: Path): Path = path.ext("thy")
     1.8 -
     1.9  
    1.10    /* header */
    1.11  
    1.12 @@ -96,18 +94,6 @@
    1.13      try { read(reader).map(Standard_System.decode_permissive_utf8) }
    1.14      finally { reader.close }
    1.15    }
    1.16 -
    1.17 -
    1.18 -  /* check */
    1.19 -
    1.20 -  def check(name: String, source: CharSequence): Thy_Header =
    1.21 -  {
    1.22 -    val header = read(source)
    1.23 -    val name1 = header.name
    1.24 -    val path = Path.explode(name)
    1.25 -    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
    1.26 -    header
    1.27 -  }
    1.28  }
    1.29  
    1.30  
    1.31 @@ -116,10 +102,5 @@
    1.32  {
    1.33    def map(f: String => String): Thy_Header =
    1.34      Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
    1.35 -
    1.36 -  def norm_deps(f: String => String, g: String => String): Thy_Header =
    1.37 -    copy(imports = imports.map(name => f(name)))
    1.38 -    // FIXME
    1.39 -    // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
    1.40  }
    1.41