--- a/src/Pure/Thy/thy_header.scala Mon Dec 26 13:28:37 2016 +0100
+++ b/src/Pure/Thy/thy_header.scala Mon Dec 26 15:31:13 2016 +0100
@@ -69,7 +69,7 @@
Outer_Syntax.init().add_keywords(bootstrap_header)
- /* file name */
+ /* file name vs. theory name */
val PURE = "Pure"
val ML_BOOTSTRAP = "ML_Bootstrap"
@@ -94,6 +94,12 @@
case _ => None
}
+ def is_ml_root(theory: String): Boolean =
+ ml_roots.exists({ case (_, b) => b == theory })
+
+ def is_bootstrap(theory: String): Boolean =
+ bootstrap_thys.exists({ case (_, b) => b == theory })
+
/* header */