src/Pure/Thy/thy_header.scala
changeset 67212 f5d44a01030c
parent 67164 39f57f0757f1
child 67215 03d0c958d65a
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Dec 16 14:24:12 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Dec 16 14:40:21 2017 +0100
     1.3 @@ -79,21 +79,21 @@
     1.4    val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
     1.5  
     1.6    private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     1.7 -  private val Import_Name = new Regex(""".*?([^/\\:]+)""")
     1.8 +  private val File_Name = new Regex(""".*?([^/\\:]+)""")
     1.9  
    1.10    def is_base_name(s: String): Boolean =
    1.11      s != "" && !s.exists("/\\:".contains(_))
    1.12  
    1.13    def import_name(s: String): String =
    1.14      s match {
    1.15 -      case Import_Name(name) if !name.endsWith(".thy") => name
    1.16 +      case File_Name(name) if !name.endsWith(".thy") => name
    1.17        case _ => error("Malformed theory import: " + quote(s))
    1.18      }
    1.19  
    1.20    def theory_name(s: String): String =
    1.21      s match {
    1.22        case Thy_File_Name(name) => bootstrap_name(name)
    1.23 -      case Import_Name(name) =>
    1.24 +      case File_Name(name) =>
    1.25          ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    1.26        case _ => ""
    1.27      }