src/Pure/Thy/thy_header.scala
changeset 66195 bb886f13623a
parent 65539 dbcd9b3e1b49
child 66713 afba7ffd6492
     1.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jun 26 11:07:48 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jun 26 15:57:20 2017 +0200
     1.3 @@ -89,8 +89,7 @@
     1.4  
     1.5    def theory_name(s: String): String =
     1.6      s match {
     1.7 -      case Thy_File_Name(name) =>
     1.8 -        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
     1.9 +      case Thy_File_Name(name) => bootstrap_name(name)
    1.10        case Import_Name(name) =>
    1.11          ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    1.12        case _ => ""
    1.13 @@ -102,6 +101,9 @@
    1.14    def is_bootstrap(theory: String): Boolean =
    1.15      bootstrap_thys.exists({ case (_, b) => b == theory })
    1.16  
    1.17 +  def bootstrap_name(theory: String): String =
    1.18 +    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
    1.19 +
    1.20  
    1.21    /* header */
    1.22