src/Pure/Thy/thy_header.scala
changeset 67215 03d0c958d65a
parent 67212 f5d44a01030c
child 67290 98b6cd12f963
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Dec 16 15:15:51 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Dec 16 16:46:01 2017 +0100
     1.3 @@ -76,7 +76,8 @@
     1.4    val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
     1.5    val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
     1.6  
     1.7 -  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
     1.8 +  val bootstrap_global_theories =
     1.9 +    (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
    1.10  
    1.11    private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    1.12    private val File_Name = new Regex(""".*?([^/\\:]+)""")
    1.13 @@ -94,7 +95,8 @@
    1.14      s match {
    1.15        case Thy_File_Name(name) => bootstrap_name(name)
    1.16        case File_Name(name) =>
    1.17 -        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    1.18 +        if (name == Sessions.root_name) name
    1.19 +        else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
    1.20        case _ => ""
    1.21      }
    1.22