--- a/src/Pure/Thy/sessions.scala Mon Apr 17 12:29:50 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 17 13:14:01 2017 +0200
@@ -387,7 +387,7 @@
if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
def global_theories: Map[String, String] =
- (Map.empty[String, String] /:
+ (Thy_Header.bootstrap_global_theories.toMap /:
(for {
(session_name, (info, _)) <- imports_graph.iterator
thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
--- a/src/Pure/Thy/thy_header.scala Mon Apr 17 12:29:50 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Apr 17 13:14:01 2017 +0200
@@ -73,10 +73,11 @@
val PURE = "Pure"
val ML_BOOTSTRAP = "ML_Bootstrap"
- val ML_ROOT = "ML_Root"
- val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
+ val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
+ val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
+
private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
private val Import_Name = new Regex(""".*?([^/\\:]+)""")